# LLM Framework for Discovering Major Mathematical Conjectures: AI's Quest for the Next Riemann Hypothesis

arXiv: https://arxiv.org/abs/2607.28632 · HTML: https://mlsanity.com/paper/2607.28632/

## Key facts

- Cited by 1 papers in the map (data through 14 Oct 2026).
- Builds on 25 of its 34 references that are in the map.
- First posted on arXiv 19 Apr 2026.

## Builds on (most cited first, 25 of 25)

- [Reflexion: Language Agents with Verbal Reinforcement Learning](https://mlsanity.com/paper/2303.11366/) (2023)
- [Self-Refine: Iterative Refinement with Self-Feedback](https://mlsanity.com/paper/2303.17651/) (2023)
- [Solving Quantitative Reasoning Problems with Language Models](https://mlsanity.com/paper/2206.14858/) (2022)
- [The AI Scientist: Towards Fully Automated Open-Ended Scientific Discovery](https://mlsanity.com/paper/2408.06292/) (2024)
- [LeanDojo: Theorem Proving with Retrieval-Augmented Language Models](https://mlsanity.com/paper/2306.15626/) (2023)
- [The AI Scientist-v2: Workshop-Level Automated Scientific Discovery via Agentic Tree Search](https://mlsanity.com/paper/2504.08066/) (2025)
- [ScienceAgentBench: Toward Rigorous Assessment of Language Agents for Data-Driven Scientific Discovery](https://mlsanity.com/paper/2410.05080/) (2024)
- [DeepSeek-Prover: Advancing Theorem Proving in LLMs through Large-Scale Synthetic Data](https://mlsanity.com/paper/2405.14333/) (2024)
- [DeepSeek-Prover-V1.5: Harnessing Proof Assistant Feedback for Reinforcement Learning and Monte-Carlo Tree Search](https://mlsanity.com/paper/2408.08152/) (2024)
- [LLM-SR: Scientific Equation Discovery via Programming with Large Language Models](https://mlsanity.com/paper/2404.18400/) (2024)
- [MLGym: A New Framework and Benchmark for Advancing AI Research Agents](https://mlsanity.com/paper/2502.14499/) (2025)
- [Mathematical exploration and discovery at scale](https://mlsanity.com/paper/2511.02864/) (2025)
- [Lean-STaR: Learning to Interleave Thinking and Proving](https://mlsanity.com/paper/2407.10040/) (2024)
- [TheoremLlama: Transforming General-Purpose LLMs into Lean4 Experts](https://mlsanity.com/paper/2407.03203/) (2024)
- [Constructions in combinatorics via neural networks](https://mlsanity.com/paper/2104.14516/) (2021)
- [Automated Statistical Model Discovery with Language Models](https://mlsanity.com/paper/2402.17879/) (2024)
- [LeanAgent: Lifelong Learning for Formal Theorem Proving](https://mlsanity.com/paper/2410.06209/) (2024)
- [PatternBoost: Constructions in Mathematics with a Little Help from AI](https://mlsanity.com/paper/2411.00566/) (2024)
- [Mathesis: Towards Formal Theorem Proving from Natural Languages](https://mlsanity.com/paper/2506.07047/) (2025)
- [ProofBridge: Auto-Formalization of Natural Language Proofs in Lean via Joint Embeddings](https://mlsanity.com/paper/2510.15681/) (2025)
- [miniF2F-Lean Revisited: Reviewing Limitations and Charting a Path Forward](https://mlsanity.com/paper/2511.03108/) (2025)
- [Advancing Geometry with AI: Multi-agent Generation of Polytopes](https://mlsanity.com/paper/2502.05199/) (2025)
- [FormaRL: Enhancing Autoformalization with no Labeled Data](https://mlsanity.com/paper/2508.18914/) (2025)
- [LeanConjecturer: Automatic Generation of Mathematical Conjectures for Theorem Proving](https://mlsanity.com/paper/2506.22005/) (2025)
- [Lean-ing on Quality: How High-Quality Data Beats Diverse Multilingual Data in AutoFormalization](https://mlsanity.com/paper/2502.15795/) (2025)

## Built on by (most cited first, 1 of 1)

- [LANTERN: Illuminating Hidden Mathematical Knowledge in Language Models](https://mlsanity.com/paper/2609.32264/) (2026)

## Abstract (arXiv)

Major mathematical conjectures still depend heavily on expert intuition, so a unified method for the systematic generation and validation of conjectures with substantial mathematical potential remains unavailable. We present a three stage pipeline for major conjecture discovery, with region search from explicit local evidence modules, reflective validation for foundationality, novelty, and potential significance, and formal validation in Lean 4 and Mathlib. The objective is the discovery of mathematical problems with high problem taste, namely problems whose proofs could reorganize the language of a research area and provide durable help to human mathematical research. Experiments on twenty candidates showstable passage from natural language to formal checks, with twenty out of twenty candidates passing Lean parsing and type checking, twenty out of twenty candidates not directly absorbed by exact?,twenty out of twenty candidates not automatically discharged by aesop, and no explicit duplicates or near duplicates.