Mathematical foundations, decidability, proof systems, and AI-assisted formalization.
13 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-11OpenAI reports that no algorithm can decide whether an integer-coefficient polynomial has a rational solution when the number of variables is part of the input.
Read original source Original manuscript: claim, hypotheses, and contextgithub.com
Original report: 2026-10-06OpenAI reports that every order automorphism of the full Turing-degree partial order is the identity in ZFC, without a definability or regularity restriction on the automorphism.
Read original source Original manuscript: claim, hypotheses, and contextgithub.com
Original report: 2026-10-06OpenAI reports that consistency of ZF implies consistency of ZF plus the Partition Principle and Choice for ordinal-indexed families but without the full Axiom of Choice.
Read original source Original manuscript: claim, hypotheses, and contextgithub.com
Original report: 2026-10-06Alman 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-19OpenAI claims that every infinite Löwenheim–Skolem bound admits a uniform threshold above which one categorical cardinal forces categoricity throughout the remaining tail, in ZFC.
Read original source Pinned primary manuscript · family 240github.com
Original report: 2026-10-06Anthropic 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-25Mathematical foundations, decidability, proof systems, and AI-assisted formalization.
Related focused topics and problems retain their own statements and baselines. A contribution may belong to more than one field; it is counted once within each topic.
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.
