Axiom Math announced that its artificial intelligence (AI) system called AxiomProver has completed a machine-checkable formalization of the BGP246 theorem. Formalization means converting a mathematical argument into a precise form that a computer can examine step by step to confirm every detail is correct. The BGP246 theorem states that there are infinitely many pairs of prime numbers that differ by at most 246. This is the closest proven bound to the twin prime conjecture, which is the still-unproven claim that infinitely many pairs of primes differ by exactly two.
The announcement thread on X note that in 2013 Yitang Zhang first showed infinitely many primes lie within 70 million of each other. James Maynard later reduced the gap to 600. A large collaboration then brought the gap down to 246, a record that has stood for twelve years. AxiomProver has now verified this result in the computer language Lean, conditional on an established result known as the Bombieri-Vinogradov theorem. Axiom Math has released reusable components as an open library so others can inspect and build on it.
Background on the mathematical result
The article published on IEEE Spectrum mentioned in the announcement explains that this formalization marks a notable step in AI-assisted mathematics. The article describes how the 246 theorem sits at the current limit of what is known about close pairs of primes. It recounts the same history of successive improvements and notes that AxiomProver produced the Lean proofs based on existing mathematical libraries. Axiom Math’s founding mathematician is quoted saying the theorem represents the threshold of human knowledge about prime numbers. The article points out that the techniques involved in number theory also underpin modern cryptography and data security. It further observes that reliable formal verification of mathematical statements may eventually help check the correctness of computer code generated by artificial intelligence systems, reducing risks from errors.
Taken together, the announcement and the reporting show that AI systems are becoming capable of handling substantial formal proofs in advanced mathematics. This progress indicates that AI-assisted mathematics is advancing fast.