Anthropic's Claude Refutes the Exponential Time Hypothesis, With a Lean Proof (GitHub Repo)
Summary
Anthropic 发布 formal-math GitHub 仓库，收录机器验证的 Lean 4 形式化证明，其中 Claude 生成的证明在 Lean 中形式化了一个计数 k-CNF 满足赋值的算法，从而推翻指数时间假设（ETH），并包含 Riemann zeta 零点与 3SUM/APSP 等结果的形式化。
View Cached Full Text
Cached at: 10/29/26, 01:24 AM
anthropics/formal-math
Source: https://github.com/anthropics/formal-math
formal-math
Machine-checked Lean 4 formalizations published by Anthropic. Each subdirectory is a self-contained Lake project with its own toolchain pin, README and build instructions; build from inside the subdirectory. Projects follow the layout of the Palomar submission template (Challenge.lean / Solution.lean / comparator.json / formalization.yaml at the project root) and are submitted to Palomar with the subdirectory as the selected project; the licence file Palomar reads is this repository’s root LICENSE.
| Project | Statement | Lean / Mathlib |
|---|---|---|
zeta23/ | More than two thirds of the zeros of the Riemann zeta function are simple and on the critical line (Alpöge–Furman, arXiv:2608.13637) | leanprover/lean4:v4.33.0-rc2 / Mathlib v4.33.0-rc2 |
3sum-apsp/ | Programs of a word RAM solve 3SUM in O(n^1.9992) steps and the (min,+)-product and APSP in O(n^2.99942) steps, on integers of polynomial size; also bounds for Exact Triangle and Zero-Weight k-Clique, and further results of the paper, item by item (Alman–Vassilevska Williams, arXiv:2610.06783) | leanprover/lean4:v4.33.1 / Mathlib v4.33.1 |
eth/ | One deterministic Turing machine counts the satisfying assignments of every k-CNF with m ≥ 2 clauses on n ≥ 4 variables, each of which occurs, in 2^O(min{k^2 n log log n/√log n, km/√log m}) steps, which refutes the Exponential Time Hypothesis (Claude, paper in the folder) | leanprover/lean4:v4.33.1 / Mathlib v4.33.1 |
CI
Pull requests and pushes to main run .github/workflows/lean-projects.yml on each project folder whose files changed, and only on those; a change confined to CI configuration or documentation (.github/, this README, …) verifies nothing, and a full run of every project is started manually from the Actions tab (workflow_dispatch, projects = all). The verify job runs on the runner label in the repository/organization variable LEAN_CI_RUNNER when it is set (e.g. a GitHub larger runner such as ubuntu-latest-16-cores), otherwise on ubuntu-latest. Pull-request runs reuse the project’s previous Lake build for the same toolchain and manifest (only changed modules are rebuilt); merges to main and manual runs build from scratch. A project passes when lake build succeeds on its pinned toolchain with no sorry outside the trusted comparator statement files (Challenge.lean, Challenge/<Topic>.lean), and when the Palomar registry’s acceptance check — leanprover/comparator with a toolchain-matched lean4export, the independent nanoda kernel and the landrun sandbox, at the registry’s tool pins — prints Your solution is okay! for every comparator configuration the project declares (.github/scripts/comparator-check.sh; run it locally with cd <project> && bash ../.github/scripts/comparator-check.sh).
To add a project: create a top-level directory with lakefile.toml (or lakefile.lean), lean-toolchain, lake-manifest.json, a Mathlib-only Challenge module stating the headline theorems, a Solution module proving them from the library, and at least one comparator configuration (comparator.json next to the lakefile, or comparator/config*.json); add a row to the table above.
License
Apache-2.0 — see LICENSE. Individual projects may carry additional NOTICE files.
Similar Articles
Internal Claude research model also independently refuted the Exponential Time Hypothesis on October 16, with 14M output tokens and no human input.
Anthropic 的内部 Claude 研究模型在 10 月 16 日独立推翻了指数时间假设(ETH)，使用了 1400 万输出 token 且无人工输入，相关证明已发布在 GitHub 上。
The Exponential Time Hypothesis Is False [pdf]
OpenAI released a repository of 721 mathematical manuscripts generated by an unnamed internal model, including a claimed refutation of the Exponential Time Hypothesis, with about 42% of results formalized in Lean along with abridged reasoning traces.
Understanding the Exponential Time Hypothesis, and OpenAI's claim that it is false
OpenAI 宣称发布了一篇证明指数时间假设（ETH）为假的论文，主定理已通过 Lean 验证，并由 Impagliazzo、Paturi 和 Williams 领导的独立工作组进行审查；文章通俗解释了 3-SAT、NP 完全性以及 ETH 被证伪可能带来的深远影响。
OpenAI and Anthropic both claim 3-SAT in 2^o(n) time, refuting the Exponential Time Hypothesis — a 43-min explainer made with Claude
OpenAI and Anthropic both claim their internal AI models independently refuted the Exponential Time Hypothesis by solving 3-SAT in 2^o(n) time, a result with Lean certificates but not yet reviewed by human experts. The article is a 43-minute explainer covering the two proofs, their galactic runtime, and how to read such claims.
Frontier AI labs say their models refuted the Exponential Time Hypothesis. What does that mean?
OpenAI released proofs claiming to refute the Exponential Time Hypothesis, prompting Anthropic to publish its own refutation and leading computer scientists to organize community review of the AI-generated results.