用AI系统化发现高价值数学猜想，推动数学研究范式革新。
LLM Framework for Discovering Major Mathematical Conjectures: AI's Quest for the Next Riemann Hypothesis
- 构建三阶段流程：从局部证据搜寻到反思验证，再到形式化证明
- 20个候选猜想全部通过Lean 4语法与类型检查，无重复或近似项
- 聚焦‘问题品味’高的猜想，有望重塑领域语言与研究范式
重大数学猜想仍严重依赖专家直觉，缺乏系统生成与验证的统一方法。本文提出三阶段猜想发现框架：基于显式局部证据的区域搜索、对基础性、新颖性与潜在重要性的反思验证，以及在Lean 4和Mathlib中的形式化验证。目标是发现具有高“问题品味”的数学问题，即其证明可能重构某一研究领域的语言体系，并为人类数学研究提供持久助力。对20个候选猜想的实验表明，从自然语言到形式化检查的转换稳定可行：20个全部通过Lean解析与类型检查，20个未被exact?直接吸收，20个未被aesop自动求解，且无显式重复或近似重复项。
原文摘要 · Abstract (English)
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.
Thank you to arXiv for use of its open access interoperability. PaperDance 不是 arXiv 官方产品；中文卡片由大模型生成，请以原文为准。