AxiomProver formalizes the 246 prime-gap theorem

Axiom Math’s AxiomProver has produced a machine-checked Lean 4 formalization of the theorem that infinitely many pairs of primes differ by at most 246, the strongest known bounded-gap result. The team published an interactive formalization of the BGP246 theorem and the reusable PrimeGapsLib; IEEE Spectrum’s account notes that the system formalized Maynard and Polymath8b’s result rather than proving the still-open twin-prime conjecture. For builders, the useful artifact is not a chatbot’s confident answer but a reusable proof pipeline whose output a small trusted kernel can check; OpenAI’s independently verified math result shows why that distinction is becoming the credibility standard.