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

[Submitted on 19 Apr 2026]

View PDF HTML (experimental)

Abstract: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.

Submission history

From: Zixin Zeng [view email]
[v1] Sun, 19 Apr 2026 11:13:41 UTC (1,319 KB)