Anthropic publishes a 3-SAT algorithm found by an internal Claude research model: its paper and Lean 4 proof claim to refute the Exponential Time Hypothesis
Anthropic published the paper "A 2^o(n) Time Algorithm for 3-SAT" (credited to Claude, Anthropic) and an AI-written Lean 4 formalization in its official anthropics/formal-math GitHub repo. It claims a deterministic algorithm solves 3-SAT in 2^o(n) time, which would refute the Exponential Time Hypothesis (ETH). Anthropic's Levent Alpoge said on X that an internal Claude research model found the core algorithm on Oct 16 with 14M output tokens and no human input. The repo stresses the result is purely asymptotic and says nothing about solving formulas in practice.
Key Takeaways
- The paper claims a deterministic algorithm decides 3-SAT on n variables in 2^o(n) time, refuting ETH, and solves the harder counting problem #3-SAT in 2^O(n log log n / sqrt(log n)) time
- Per Levent Alpoge on X, an internal Claude research model found the core algorithm on Oct 16 with 14M output tokens and no human input; researchers then worked with Claude on the presentation
- The Lean 4 proof was written by AI models and pins Lean and Mathlib v4.33.1; the README says it depends only on Lean's three standard axioms, and CI re-checks it with a second independent kernel, nanoda
- The repo states the result is purely asymptotic and says nothing about solving formulas in practice; independent review by mathematicians is still pending
- A day earlier OpenAI announced its own model-produced refutation of ETH; both claims are now under review
Linked Models & Agents:
