For decades, mathematicians have dreamed of a world where computers could do more than just crunch numbers—where they could actually think, reason, and help discover new truths. A major hurdle, however, has been the notorious “hallucination” problem of artificial intelligence: large language models (LLMs) are great at sounding confident, but they frequently make mathematical errors, making them unreliable for serious research.

Now, a groundbreaking study by researchers including Tsoukalas et al., published in Science, has shattered that barrier by combining the creative writing power of AI with the ruthless accuracy of a mathematical referee.

Their system—called AlphaProof Nexus—pioneers a new way of doing math by teaming up an AI with a specialized computer program called Lean is a “formal proof assistant,” a piece of software that acts as the ultimate skeptic. It doesn’t accept a mathematical proof unless every single logical step is airtight and verified by its strict compiler.

The endless loop of creativity and proof.

The magic of AlphaProof Nexus lies in its teamwork model:

1. The AI brainstorms: The large language model acts as the creative mathematician, generating ideas, strategies, and formal proofs in the Lean language.

2. The computer checks: The Lean compiler instantly tests the AI’s work. If there’s even a tiny flaw in the logic, it rejects it and points out why.

3. The AI learns and repeats: The AI takes that feedback, corrects its mistakes, tries a different angle, and loops through the process autonomously thousands of times until it finds a winning proof.

Real Breakthroughs, Real History.

This isn’t just about solving homework problems or beating math competitions. In this large-scale deployment, the AI agent tackled genuine, unsolved mysteries in mathematics—and won:

* Cracking Erdős Problems: It successfully resolved 9 out of 353 open problems posed by the legendary mathematician Paul Erdős, including two that had stumped human mathematicians for 56 years.

* Tackling Integer Sequences: It proved 44 out of 492 open conjectures from the On-Line Encyclopedia of Integer Sequences (OEIS).

* Expanding Frontiers: It successfully resolved an open question in algebraic geometry and even improved a known mathematical bound in min-max optimization.

What this means for the future.

This breakthrough marks a major turning point. By coupling the imaginative generation of LLMs with the infallible checking of automated proof assistants, AI is transitioning from a clever conversationalist into a genuine research partner.

We are entering an era where AI doesn’t just guess the next word—it helps push the boundaries of human knowledge, opening up new horizons in combinatorics, graph theory, quantum optics, and beyond.

While the results from Tsoukalas et al. (* Science*, 2026) represent a major milestone for AI-assisted research, examining the paper critically reveals several key limitations and caveats regarding the current state of autonomous formal proof search:

1. Low Overall Yield (2.5% Success Rate)

* The Numbers: The agent solved 9 out of 353 open Erdős problems attempted (~2.5%) and 44 out of 492 OEIS conjectures (~8.9%).

* The Reality: The system fails or gets stuck on the vast majority (~97.5%) of problems. It primarily succeeds on sub-problems that lend themselves well to recursive combinatorial search, specific explicit constructions, or algorithmic case checking.

2. High Computational & Financial Cost.

* Expensive Inference: The paper reports that successfully resolving a single hard Erdős problem cost several hundred dollars in computing inference per problem.

* Scaling Bottleneck: Running brute-force or evolutionary proof search over thousands of iterations across complex formal goal states requires massive compute budgets, making this approach currently inaccessible for independent academic researchers without industrial GPU clusters.

3. Dependency on Human Formalization (The “Translation” Bottleneck)

* Prerequisite Formalization: The open problems had to be manually translated into Lean before the agent could attempt them.

* The Real Bottleneck: Translating messy, intuitive, high-level natural language math into rigorous, machine-readable Lean code remains an arduous human task. The AI agent did not read textbook math papers directly and solve them; it operated strictly within pre-formalized benchmark environments.

4. Selection Bias in Solved Problems.

* Type of Math: Many of the resolved conjectures (such as specific OEIS series or combinatorial identity bounds) represent relatively niche or incremental questions rather than grand conceptual breakthroughs.

* Lack of Novel Conceptual Frameworks: LLM proof search excels at executing clever combinations of known techniques or finding obscure modular cases, but it still struggles to invent fundamentally new core mathematical concepts or abstractions (e.g., creating entirely new theories).

5. Verification vs. Human Comprehensibility.

* Machine-Verified, but Hard to Read: Lean guarantees that every step of the generated proof is logically sound (no hallucinations). However, computer-generated formal code is often thousands of lines long and opaque, requiring human mathematicians to perform significant post-hoc effort to translate the machine proof back into clear, insightful natural-language mathematics.

Summary Perspective.

AlphaProof Nexus proves that formal verification eliminates AI hallucinations in pure math. However, rather than demonstrating an autonomous “mathematician,” it highlights a brute-force proof searcher—exceptionally effective when given a clear, pre-formalized search space and substantial compute, but limited in broad conceptual discovery and cost efficiency.

#ArtificialIntelligence #mathematics #formalverification #Lean4 #LLM #AIAgents

Large language models (LLMs) increasingly excel at mathematics tasks, but their unreliability limits their utility in mathematics research. A mitigation is to use LLMs to generate formal proofs in languages such as Lean, in which the compiler verifies every proof step. We present the first demonstration of this method’s value in solving open problems at scale. We built an artificial intelligence agent for formal proof search that autonomously resolved nine of 353 open Erdős problems, proved 44/492 On-Line Encyclopedia of Integer Sequences conjectures, and is being deployed in combinatorics, optimization, graph theory, algebraic geometry, and quantum optics research. Even a basic agent alternating LLM-based generation with Lean-based verification replicated the Erdős successes. These findings demonstrate the power of formal proof search as an enabler of autonomous mathematical discovery.