Just a week after an AI disproved an 80-year-old conjecture and astonished mathematicians, another conjecture that had stood for half a century has fallen, inspired by the same techniques, but this time written entirely by humans. Last week, an unreleased AI model from OpenAI disproved an important conjecture first posed by Hungarian mathematician Paul Erdős, called the unit distance problem. The puzzle, which Erdős considered his "most striking contribution to geometry" and which many mathematicians had failed to unravel, concerns the number of similar-sized connections you can make between dots arranged on a flat surface. Erdős had set an upper ceiling on this number, which many experts had assumed was correct. But the AI model showed that this number could in fact be much larger, using an obscure trick from algebraic number theory to make complex structures with extremely high dimensions, which could then be used to arrange the dots in a very different arrangement than humans had considered.

Mathematicians stunned by AI's biggest breakthrough in mathematics yet An 80-year-old maths conjecture that has eluded the world's greatest mathematicians has been cracked by an artificial intelligence model built by OpenAI. The result has stunned experts and is being hailed as a seismic moment for AI's mathematical ability. "This is a problem that I didn't expect to see solved in my lifetime," says Misha Rudnev at the University of Bristol, UK. "It's absolutely a bomb." Tim Gowers at the University of Cambridge wrote that the solution is "a milestone in AI mathematics" in a blog post accompanying the work . "If a human had written the paper and submitted it to the and I had been asked for a quick opinion, I would have recommended acceptance without any hesitation. No previous AI-generated proof has come close to that."

One of the most bitterly contested proofs in modern mathematics may be on the verge of being untangled. Two projects, both aiming to use a computer program to cast new light on the controversy, are now up and running - with one having operated in secret for more than two years already. The developments are a positive sign that the row might find a solution, say mathematicians. The saga began in 2012 when Shinichi Mochizuki at Kyoto University, Japan, claimed to have proved a famous idea called the ABC conjecture, posting a 500-page proof online. The conjecture is simple to state, concerning prime numbers involved in solutions to the equation a + b = c and how these numbers relate to each other.

How did humanity coax mathematics from the aether? We explore the Platonic view that mathematics can be discovered from its axioms---a game of conjecture and proof. We describe an agent that jointly learns to pose challenging problems for itself (conjecturing) and solve them (theorem proving). Given a mathematical domain axiomatized in dependent type theory, we first combine methods for constrained decoding and type-directed synthesis to sample valid conjectures from a language model. Our method guarantees well-formed conjectures by construction, even as we start with a randomly initialized model. We use the same model to represent a policy and value function for guiding proof search. Our agent targets generating hard but provable conjectures --- a moving target, since its own theorem proving ability also improves as it trains. We propose novel methods for hindsight relabeling on proof search trees to significantly improve the agent's sample efficiency in both tasks. Experiments on 3 axiomatic domains (propositional logic, arithmetic and group theory) demonstrate that our agent can bootstrap from only the axioms, self-improving in generating true and challenging conjectures and in finding proofs.

Recent advances in automated theorem proving leverages language models to explore expanded search spaces by step-by-step proof generation. However, such approaches are usually based on short-sighted heuristics (e.g., log probability or value function scores) that potentially lead to suboptimal or even distracting sub-goals, preventing us from finding longer proofs. To address this challenge, we propose POETRY (PrOvE Theorems RecursivelY), which proves theorems in a recursive, level-by-level manner in the Isabelle theorem prover. Unlike previous step-by-step methods, POETRY searches for a verifiable sketch of the proof at each level and focuses on solving the current level's theorem or conjecture. Detailed proofs of intermediate conjectures within the sketch are temporarily replaced by a placeholder tactic called sorry, deferring their proofs to subsequent levels. This approach allows the theorem to be tackled incrementally by outlining the overall theorem at the first level and then solving the intermediate conjectures at deeper levels. Experiments are conducted on the miniF2F and PISA datasets and significant performance gains are observed in our POETRY approach over state-of-the-art methods. POETRY on miniF2F achieves an average proving success rate improvement of 5. 1% . Moreover, we observe a substantial increase in the maximum proof length found by POETRY, from 10 to 26 .

How did humanity coax mathematics from the æther?