**摘要**
与证明助手相结合的人工智能系统现在可以大规模生成形式数学，检查者可以验证的内容与数学家所重视的内容之间的差距已经成为约束约束。我们将有价值的数学生成建模为极限中的嵌套语言生成：可验证的正式语言$ F $ ，通过成员资格预言机（证明检查器）访问，包含一个unkno
👤 作者: Xiaoyu Li, Andi Han, Dai Shi, Zheng Gao, Jiaojiao Jiang, Junbin Gao

---
🔗 **[Flood and Harvest: The Provable Necessity of Trivia for Generating Valuable Mathematics via the Lens of Language Generation in the Limit](https://arxiv.org/abs/2606.14688v1)**

> Flood and Harvest: The Provable Necessity of Trivia for Generating Valuable Mathematics via the Lens of Language Generation in the Limit
🏷️ 来源: ArXiv cs.AI
⏱️ 2026-06-15 14:00