Topic · 10 stories
10 stories tagged mathematics on AI Tamer, newest first.
OpenAI claims three new AI results, including a refutation of ETH, now public on GitHub with a Lean proof. None is peer reviewed, and its math advisers object.
A 17 October guest post on Terence Tao's blog proposes a math journal that requires proofs formally verified in Lean, citing errors in LLM-assisted proofs.
Tao says Open Math OS is soft-launched with DeepSeek V4.1 Flash, Kimi K3, and GLM 5.3 Flash on donated compute. Free academic accounts are still being granted.
Shanghai AI Lab says Intern-S2 helped on a 3D Ghys case. Zhang's preprint states a codimension-one theorem. Lean checks four theorems, one hypothesis open.
A King's College London and Cambridge preprint argues that OpenAI's Lean files for a Navier-Stokes blow-up proof do not match the English argument. The authors do not judge whether that English proof is correct.
doubleAI's October 2026 paper states an 8/5 girth constant for explicit regular graphs, above the 1988 bound of 4/3. The PDF is not a journal article. Ctech says the company puts the compute under $2,000.
A Charles University paper describes Bolzano, a multi-agent prover the authors say solved about 200 of about 3,800 open problems. Most counts are estimates. Four STOC 2026 answers were confirmed by those papers' authors.
OpenAI's math repository withdrew three manuscripts after a sign error, revised 14 others, and updated citations in 13 more. The README now lists 719 manuscripts, with 300 of 719 top-line results Lean-formalized.
OpenAI's GitHub catalogue lists 722 math manuscripts in 372 families from an unreleased internal model. Not all have Lean checks, and OpenAI says some unformalized results could have issues.
On 6 October, Thomas Bloom writes on Terence Tao's blog that he will freeze new problem comments and proof claims on the Erdos problems site and stop showing a solved count.
