Researchers propose LLM pipeline to generate and formally validate mathematical conjectures

A new arXiv preprint proposes a three-stage pipeline to systematically generate and validate mathematical conjectures with potential to reorganize research areas. The authors, led by Alizer Wong and Zixin Zeng, describe a process that begins with region search using explicit local evidence modules, followed by reflective validation for foundationality, novelty, and significance, and concludes with formal validation in Lean 4 and Mathlib.

In experiments, the authors report that all twenty candidate conjectures passed Lean parsing and type checking, none were directly absorbed by the exact? tactic, none were automatically discharged by aesop, and no explicit duplicates or near-duplicates were detected among the candidates.

The pipeline aims to produce problems with high 'problem taste'—conjectures whose proofs could reorganize the language of a research area and provide durable help to human mathematical research. The authors note that major mathematical conjectures still depend heavily on expert intuition, and a unified method for systematic generation and validation has been unavailable until now.

The preprint is titled 'LLM Framework for Discovering Major Mathematical Conjectures: AI's Quest for the Next Riemann Hypothesis' and was submitted to arXiv on April 19, 2026.