Claude-discovered 3-SAT algorithm reportedly refutes the Exponential Time Hypothesis

What the proof files are meant to check

The repository's explanation of its Lean proof says MainResults.lean states both that ETH is false and the paper's main counting-algorithm theorem. It provides build instructions and describes a fuller check using a second proof-checking system. But the README also draws a distinction: Lean checks proofs, while “no machine checks that this file says what the paper says.” That correspondence remains a question for a reader to check, not something established by the listed commands alone.

A separate Oct. 27 post by @alpoge quotes a statement saying the core algorithm was found Oct. 16 using 14 million output tokens and no human input. The post says Anthropic researchers then worked with Claude on the paper's presentation. The Oct. 16 date, token details and account of human involvement do not appear in the repository's README, and the linked GitHub page for the PDF displays a file wrapper rather than the paper's text. Reacting to the post, @AndrewCurran_ called the claim “extremely confusing.”