Major mathematical conjectures have long depended on the intuition of human experts, with no unified method available for the systematic generation and validation of high-potential problems. A new research paper published on arXiv proposes an LLM-based framework designed to discover conjectures with "high problem taste"—those whose eventual proofs could reorganize the language of a research area and provide durable assistance to human mathematicians.
A Three-Stage Pipeline
The researchers introduced a structured approach to ensure that AI-generated conjectures are both mathematically sound and significant. The pipeline consists of:
- Region Search: Utilizing explicit local evidence modules to identify areas of interest.
- Reflective Validation: Assessing the candidates for foundationality, novelty, and potential significance.
- Formal Validation: Implementing checks within Lean 4 and Mathlib to verify the mathematical structure.
Experimental Findings
The framework was tested on twenty candidates, demonstrating a stable transition from natural language descriptions to formal mathematical checks. All twenty candidates successfully passed Lean parsing and type checking. Notably, none of the candidates were directly absorbed by the exact? tactic or automatically discharged by aesop, suggesting that the framework generates non-trivial conjectures that are not already present in existing automated theorem-proving libraries.
The study emphasizes that the objective is not merely to generate conjectures, but to identify those that possess the potential to reshape mathematical research fields, much like the Riemann Hypothesis has done for number theory.
