AxiomProver Completes Lean Formalization of BGP246

Axiom Math announced that its AxiomProver system completed a machine-checkable formalization in Lean of the BGP246 theorem. The result is the best-known bound on recurring small gaps between primes and the closest approach yet to the Twin Prime Conjecture. Company founder Carina Hong called it the team's first large-scale Lean formalization. Mathematician Ken Ono posted a link to the public project for others to use. Axiom Math scheduled an appearance on MTSlive the same day to discuss the work with Carina Hong and a colleague.