用大模型自动生成高等数学猜想，助力自动定理证明。
LeanConjecturer: Automatic Generation of Mathematical Conjectures for Theorem Proving
- 结合规则提取与大模型生成，从40个基础文件中产生成百上千条猜想。
- 平均每文件生成103条新猜想，其中3776条有效且非平凡。
- 可为强化学习提供训练数据，推动拓扑等领域的新发现。
我们提出LeanConjecturer，一个在Lean 4中自动生成大学级别数学猜想的流程。该方法融合基于规则的上下文提取与大模型驱动的定理陈述生成，缓解形式化定理证明中的数据稀缺问题。通过迭代生成与评估，系统从40个Mathlib种子文件中生成12,289条猜想，其中3,776条为语法正确且非平凡（无法被aesop策略证明）。我们展示了这些生成猜想在强化学习中的应用，通过组相对策略优化（GRPO）训练，显著提升定理证明能力。平均每个种子文件生成103.25条新猜想，提供了可扩展的训练数据生成方案。系统成功验证了拓扑中半开集、α开集及预开集等非平凡性质，展现出超越现有结果的数学发现潜力。
原文摘要 · Abstract (English)
We introduce LeanConjecturer, a pipeline for automatically generating university-level mathematical conjectures in Lean 4 using Large Language Models (LLMs). Our hybrid approach combines rule-based context extraction with LLM-based theorem statement generation, addressing the data scarcity challenge in formal theorem proving. Through iterative generation and evaluation, LeanConjecturer produced 12,289 conjectures from 40 Mathlib seed files, with 3,776 identified as syntactically valid and non-trivial, that is, cannot be proven by \texttt{aesop} tactic. We demonstrate the utility of these generated conjectures for reinforcement learning through Group Relative Policy Optimization (GRPO), showing that targeted training on domain-specific conjectures can enhance theorem proving capabilities. Our approach generates 103.25 novel conjectures per seed file on average, providing a scalable solution for creating training data for theorem proving systems. Our system successfully verified several non-trivial theorems in topology, including properties of semi-open, alpha-open, and pre-open sets, demonstrating its potential for mathematical discovery beyond simple variations of existing results.
Thank you to arXiv for use of its open access interoperability. PaperDance 不是 arXiv 官方产品；中文卡片由大模型生成，请以原文为准。