lean
Terence Tao calls the AI-assisted fluid blowup proofs a breakthrough News
A day before OpenAI announced its Navier-Stokes result, Terence Tao wrote that the new AI-assisted proofs of finite-time blowup for three fluid equations are a breakthrough with a high likelihood of extending to Navier-Stokes.
OpenAI says an internal model resolved the Navier-Stokes Millennium Problem News
OpenAI published a proof, produced by about 10,000 coordinated AI agents over 88 hours, that three-dimensional fluid flow can break down in finite time, and released a machine-checked Lean formalization alongside it.
Autoformalization: turning a written proof into one a machine can check Lesson
Autoformalization is the automatic translation of ordinary mathematical prose into a formal language like Lean, so that a proof written by a human or an AI can be mechanically verified instead of merely believed.
Anthropic's Lean artifact formalizes Fermat's Last Theorem, not a new discovery News
A public Anthropic Lean repository contains a complete formalization of a classical Fermat's Last Theorem proof route, which mathematician Kevin Buzzard says compiles and checks.
Anthropic says Claude produced a complete Lean proof of Fermat's Last Theorem News
Anthropic says Claude worked largely autonomously for 11 days to produce a complete machine-checked Lean 4 proof of Fermat's Last Theorem, extending a long-running human formalization effort rather than independently rediscovering Wiles's mathematics.
Three Days On, Nobody Has Publicly Compiled OpenAI's Ten Proofs News
OpenAI's repository of Lean proofs for ten mathematics results has 434 stars and 39 forks but exactly one commit, no pull requests, and no issues, and no third party has published a build log showing the proofs check.
The non-sofic group is the one OpenAI claim a computer can check News
Chapter 3 of OpenAI's new manuscript claims to have constructed a non-sofic group, settling a long-open question, and ships roughly 34,000 lines of Lean code with no unproved placeholders so outsiders can verify it.
TorchLean Tool
A Lean 4 framework for formalizing, executing and verifying neural networks, with typed tensors, exact and finite-precision semantics, verified reverse-mode differentiation, and CROWN/LiRPA-style bound checking. Early and CPU-bound by its authors' own account, but it is the most concrete attempt yet at machine-checked robustness guarantees.
OpenAI NavierStokesAndEuler Tool
The Apache-2.0 Lean 4 formalization accompanying OpenAI's Navier-Stokes and Euler blowup claims, building against Mathlib and including a directory set up for independent proof-checking.
Lean comparator Tool
The Lean toolchain component used to independently check the formalization behind Anthropic's zeta-function result. Useful to anyone who wants machine-verified mathematics rather than a persuasive argument.
Formal Conjectures Tool
Google DeepMind's open Lean library of formally stated open mathematical conjectures, now the venue where the claimed Jacobian conjecture counterexample is being reviewed in public. A usable resource if you want machine-checkable statements of open problems rather than prose.
Anthropic Fermat's Last Theorem Lean repository Tool
A public Lean codebase for Anthropic's formalization of a classical proof route for Fermat's Last Theorem.