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

A new arXiv paper (2607.28632v1) introduces a three-stage pipeline using large language models to systematically discover major mathematical conjectures, with experiments showing 20 out of 20 candidates passed Lean 4 parsing and type checking, 20 out of 20 were not directly absorbed by exact?, and 20 out of 20 were not automatically discharged by aesop. The pipeline combines region search from local evidence, reflective validation, and formal validation in Lean 4 and Mathlib, aiming to generate problems with high 'problem taste' that could reorganize research areas.

arXiv:2607.28632v1 Announce Type: new 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.