Aug 18, 2026
AxiomProver-assisted formalization
Model / AI: AxiomProver
machine-checked (conditional formalization)self-reported (conditional formalization)
Axiom Math reports that AxiomProver generated machine-checkable Lean proofs from a human-built blueprint, followed by human curation and library work. The repository formalizes the Maynard sieve and the Polymath8b ingredients needed for the bound 246, conditional in Lean on Bombieri–Vinogradov.
Source read 2026-09-08. Read the project page and repository scope and comparator sections. The multi-hour build was not rerun.