Anthropic published a paper and Lean 4 formalization claiming that an internal research Claude model found a subexponential-time algorithm for 3-SAT. The repository also covers the harder task of counting satisfying assignments and stresses that the result is asymptotic, not a promise of faster practical solving. It provides checks using Lean and an independent verification kernel, but readers must still assess whether the formal statements match the paper. This is separate from OpenAI’s similar announcement and does not establish a solution to P versus NP or the collapse of cryptographic systems.