A 2^O(n) Time Algorithm for 3-SAT (github.com)

A groundbreaking deterministic algorithm has been developed that solves the 3-SAT problem on n variables in time \(2^{o(n)}\), challenging the long-held Exponential Time Hypothesis (ETH). This algorithm can even tackle the more complex #3-SAT problem, which counts satisfying assignments, achieving a time complexity of \(2^{O(n \log \log n / \sqrt{\log n})}\). Despite the asymptotic nature of the result, it represents a significant milestone in computational complexity theory and potentially opens new avenues for tackling NP-hard problems. The algorithm was discovered using an internal research model, Claude, and is documented alongside its formalization in Lean 4, offering an interesting intersection of AI and formal verification in mathematics. While the paper indicates that the results are primarily theoretical and not yet practical solutions for real-world 3-SAT instances, the implications for algorithm design and the study of computational limits are profound. If these findings hold up under scrutiny and formal proof, they could reshape our understanding of problem-solving in the realm of AI and computer science, particularly in relation to NP problems and the boundaries of computational feasibility.