AI 中文总结
该研究提出一种三阶段大语言模型框架，用于系统发现重要数学猜想，经实验验证其在20个候选猜想上的形式化检查表现稳定，无重复问题。
AI 中文摘要
重要数学猜想仍高度依赖专家直觉，目前缺乏一种能系统生成和验证具有重大数学潜力的猜想的统一方法。我们提出了一个用于重要猜想发现的三阶段流程：从显式局部证据模块进行区域搜索，对基础性、新颖性和潜在重要性进行反思性验证，以及在Lean 4和Mathlib中进行形式化验证。目标是发现具有高问题品位的数学问题，即其证明能够重组研究领域的语言并为人类数学研究提供持久帮助的问题。对20个候选猜想的实验显示，从自然语言到形式化检查的稳定通过情况为：20个候选均通过Lean解析和类型检查，20个均未被exact?直接吸收，20个均未被aesop自动解决，且无明确重复或近重复情况。
英文摘要
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.
Comments25pages, 1 figure
