#lean
-
Anthropic's AI Formally Proved Fermat's Last Theorem in Lean
In 11 days, an internal Anthropic model assembled a complete formalization of the proof of Fermat's Last Theorem — the last remaining item on a 20-year-old list of 100 formalization challenges.
-
Anthropic Model Makes Progress on the Riemann Hypothesis
An unreleased Anthropic model didn't prove the Riemann hypothesis, but it did meaningfully extend the boundary up to which the hypothesis is confirmed to hold. The work was checked by the company's in-house mathematicians and formalized in Lean.
-
OpenAI Announces Astra — the Model That Solved Ten Long-Standing Math Problems
OpenAI has unveiled Astra, a model not yet released, which in internal testing produced ten significant results in mathematics and theoretical computer science. The company calls it its “next major model.”
-
A False “Refutation” of the Collatz Conjecture Exposed a Bug in Lean's Kernel
A soundness bug has been found in the Lean proof system's kernel: with the help of AI, a formally accepted but incorrect “refutation” of the Collatz conjecture was constructed. Lean's author, Leonardo de Moura, has published a breakdown of what happened.