Formal proof systems check deductions expressed in a precise language.
9 records · Includes focused interests · How we rate progress
Math, Inc. reports Lean formalizations of sphere-packing optimality for the E₈ lattice in dimension eight and the Leech lattice in dimension 24, with uniqueness among periodic packings in dimension 24. The human maintainers report checking definitions, axiom dependencies and the supplied code.
Read original source Math, Inc.: reported formalization and scopemath.inc
Original report: 2026-03-02Math, Inc. reports completion of a Lean formalization of the strong prime number theorem and supporting complex-analysis infrastructure using Gauss with human guidance.
Original report: 2025-09-11Alman and Vassilevska Williams report deterministic O(n^1.9992) 3SUM on polynomial-size integers and O(n^2.9995) APSP with polynomially bounded integer weights in the word-RAM model.
Read original source Alman–Vassilevska Williams: algorithms and methodologyarxiv.org
Original report: 2026-10-05Almeida and Knudstorp report that Medvedev’s logic of finite problems is undecidable, by reducing periodic plane tiling to non-theoremhood.
Original report: 2026-09-11The artifact reports exact optimal radii and classifications of optimal packings for one through seven freely rotated unit squares in a disk.
Read original source Original researchgithub.com
Original report: 2026-10-02Braun reports more than exp(n/(32768ℓ²)) clauses for DAG-like Res(⊕) refutations of the bit pigeonhole principle, for n=2^ℓ and ℓ≥32, without depth or regularity restrictions.
Original report: 2026-09-19Anthropic reports an end-to-end Lean proof of Fermat’s Last Theorem and makes the formal development and verification instructions available.
Read original source Original announcementanthropic.com
Original report: 2026-09-04Sothanaphan’s writeup reports infinitely many factorial-divisibility triples with a+b−n in any prescribed positive logarithmic window, while a and b remain bounded away from 0 and n.
Read original source Sothanaphan’s theorem and writeuparxiv.org
Original report: 2026-01-12DeepMind reports Lean proofs for IMO 2024 problems 1, 2, and 6, and publishes the specific proof artifacts.
Read original source Original report (25 July 2024)deepmind.google
Original report: 2024-07-25Formal proof systems check deductions expressed in a precise language. AI can help translate statements or discover proof steps. Checking a formal proof establishes the stated theorem under its assumptions; humans still need to check that it represents the intended problem.
A proof assistant checks deductions in a formal language against an explicit statement, assumptions, and a trusted logical kernel. AI can propose intermediate lemmas, tactics, or translations. The checked artifact, rather than a fluent explanation, is the central evidence.
There are two checks: whether the formal deduction is valid and whether the formal theorem expresses the intended mathematical claim. Missing assumptions, an incorrectly translated definition, or an admitted lemma can break the connection. A successful compiler run must therefore be accompanied by the statement and dependency information.
Background review: 2026-10-11. Selected sources:
Publication dates and editorial changes.
Gauss: AI-assisted sphere-packing formalization in dimensions 8 and 24
Gauss: AI-assisted strong prime number theorem formalization
Claude-assisted truly subquadratic 3SUM and subcubic shortest paths
Claude: reported end-to-end Lean formalization of Fermat’s Last Theorem
Erdős #728: an AI-assisted factorial-divisibility proof and human writeup
Anthropic: Lean formalizations of 3SUM and shortest-path bounds
Claude: reported end-to-end Lean formalization of Fermat’s Last Theorem
Allow optional Google Analytics to help improve AIProofWatch? Privacy details.
