OpenAI and Anthropic have nearly simultaneously claimed that internal models refute the Exponential Time Hypothesis (ETH), first stated in 1999, and released Lean formalizations for checking. If the claims hold, many complexity and parameterized-algorithm results that assume ETH would need revisiting. Community verification is still underway; treat the announcements as claims, not settled theorems.
What Was Announced
According to public materials and discussion, both labs say their research models produced a path showing ETH is false. Anthropic’s notes state the core algorithm was found on Oct 16 by an internal Claude research model with no human input, using about 14 million output tokens, with Claude listed as sole author. OpenAI likewise posted a preprint and formalization artifacts.
Both sides also published Lean proofs—machine-checkable step logic that reduces the risk of pure natural-language “hallucinated proofs,” without replacing peer review. The same-day collision of security disclosures is covered in our sandbox escape and Mythos report. More coverage: AI News.
What ETH Is—and What Refuting It Would Mean
ETH, proposed in 1999 by Russell Impagliazzo and Ramamohan Paturi (UC San Diego), roughly says 3SAT has no subexponential-time algorithm: runtime grows exponentially with instance size and cannot be pushed fundamentally below that wall.
It is stronger and more specific than “P≠NP”: if ETH holds, P≠NP follows; refuting ETH does not prove P=NP. For two-plus decades, conditional lower bounds in graph theory, combinatorial optimization, databases, and computational biology have rested on ETH; a collapse would force re-evaluation.
ETH is not a Millennium Prize problem, but it is a pillar of fine-grained and parameterized complexity. Reactions range from “Turing-award-level if correct” to “wait for formal checks and peer review.”
Humans as Auditors and Compressors
Reports say ETH’s originators, with MIT and other groups, are auditing both Lean codebases line by line. Separately, NVIDIA senior AI architect Shiva Kintali compressed OpenAI’s 60-plus-page write-up into a ~22-page human-readable version—dropping some log-factor polish, adding examples—so peers can actually follow the argument.
The emerging split of labor: models draft and formalize at high speed; humans verify, distill, and turn the result into teachable knowledge. AI-plus-Lean pipelines are not new; see our earlier piece on Meta’s large Lean math library.
Implications for Research Practice (Pending Confirmation)
If confirmed, the story is larger than one conjecture falling: frontier models may close a discover–formalize loop on hard theory with minimal human steering. Same-window claims in math (Kakeya-adjacent narratives) and theoretical physics should be verified separately—not bundled as “three fields overturned in a day.”
A cautious reading: “prove and compute” work is accelerating under machines; human advantage may shift toward problem selection, cross-domain framing, and audit. Until community consensus forms, separate lab claim, Lean checks, and accepted theorem.
FAQ
Q: Does refuting ETH prove P=NP? A: No. ETH implies P≠NP if true; its failure does not imply P=NP—it mainly unsettles ETH-conditional lower bounds.
Q: Does a Lean proof mean the result is correct? A: Lean blocks many logical gaps, but whether definitions match the intended conjecture and the proof covers the right cases still needs expert audit and peer review.
Q: What does “zero human intervention” mean? A: Per Anthropic’s materials, the core algorithm was searched by an internal Claude research model without human input; publishing, messaging, and review still involve humans—defer to official notes and the final paper.
相关文章
