**TheoremSmith：大规模生成难题以训练 LLM 提升形式化验证能力**

_Show HN: TheoremSmith: Mass-Producing Hard Proof Problems to Train LLMs_

> TheoremSmith 是一个用于大规模生成高难度形式化证明问题的新工具，旨在通过合成训练数据提升大语言模型（LLM）在数学研究和代码形式化验证方面的表现。该工具解决了形式化验证因成本高昂而难以普及的痛点，能够高效生成前沿难度的验证任务，使 AI 辅助的数学突破和软件可靠性验证变得更加可行。

**来源信息**
- **来源**：Hacker News：AI 热帖
- **分类**：ai-models
- **发布时间**：2026-11-11 02:33（北京时间）
- **原文**：[打开原文](https://charleshuang.me/2026/09/27/theoremsmith)