New pipeline pairs LLMs with Lean 4 to hunt for major math conjectures
A new paper proposes a three-stage pipeline for discovering major mathematical conjectures, the kind of open problems that today still depend heavily on expert intuition rather than any systematic method. The first stage, called region search, draws on explicit local evidence modules to surface candidate areas of mathematics worth exploring. The second stage, reflective validation, checks each candidate conjecture for foundationality, novelty and potential significance. The third stage, formal validation, translates surviving candidates into the Lean 4 proof language and checks them against the Mathlib library.
The authors frame the pipeline's goal as finding problems with what they call high "problem taste": conjectures whose eventual proofs could reorganize the language of a research area and provide durable help to human mathematical research, rather than merely being correct or provable.
The paper reports experiments on twenty candidate conjectures produced by the pipeline. All twenty passed Lean parsing and type checking. None of the twenty were directly closed by the exact? tactic, and none were automatically discharged by the aesop tactic, two standard automated proof-search tools in the Lean and Mathlib ecosystem. The authors also report no explicit duplicates or near duplicates among the twenty candidates.
The text does not name the authors or their institutions, give a submission or publication date, describe any specific example conjecture the pipeline produced, compare the approach to prior automated-conjecture or theorem-proving systems, or explain how the twenty candidates were selected or from which mathematical areas they were drawn.
Key facts
- The pipeline has three stages: region search from local evidence modules, reflective validation for foundationality, novelty and significance, and formal validation in Lean 4 and Mathlib.
- The stated goal is conjectures with high "problem taste", meaning proofs that could reorganize a research area's language and durably help human mathematical research.
- In tests on twenty candidate conjectures, all twenty passed Lean parsing and type checking.
- None of the twenty candidates were directly closed by the exact? tactic or automatically discharged by the aesop tactic.
- The authors report no explicit duplicates or near duplicates among the twenty candidates.
Why it matters
Major mathematical conjectures, the paper argues, still rely heavily on expert intuition, and no unified method exists for systematically generating and validating conjectures with real mathematical potential. This pipeline is pitched as an attempt to close that gap by combining a language-model-driven search for promising problem regions with a formal proof checker, so that candidate conjectures are not just plausible-sounding text but statements that parse and type-check as real mathematics in Lean 4. The title's nod to the Riemann Hypothesis is a rhetorical comparison rather than a claim that the pipeline found anything of that stature.
Who it affects
The work targets mathematicians and researchers working on automated or AI-assisted discovery of open problems, as well as the formal-methods community that builds and maintains proof libraries like Mathlib. The source gives no further detail on who built the system, which institutions were involved, or which subfields of mathematics the test candidates came from.
How to use it
The source does not describe any released code, dataset, public tool or license, nor any pricing or deployment details. Based on the text alone, this is a research pipeline described in a paper, not a shipped product or service.
How solid is it
The pipeline's twenty test candidates all cleared Lean 4 parsing and type checking, and none were trivially resolved by the exact? or aesop automated tactics, which the authors treat as evidence the conjectures are not trivial restatements of existing results. No duplicates or near duplicates turned up among the twenty. That said, the sample is small, the paper as excerpted gives no comparison to prior automated-conjecture or theorem-proving systems, and passing formal type checks does not by itself establish that a conjecture is true, important or provable.
Risks and caveats
The text gives no worked example of an actual conjecture the pipeline produced, so it is not possible to judge the quality or originality of its output directly. It also does not explain how the twenty test candidates were chosen or from which areas of mathematics, leaving open whether the selection favored easier or more favorable cases. "Foundationality", "novelty" and "significance" are named as validation criteria but not defined or demonstrated with examples, and passing syntactic and type checks in Lean is a much lower bar than a conjecture proving true, useful or influential.
“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.”
— the paper