案例研究：使用 LPTP 与大语言模型证明 √2 是无理数

论文研究大语言模型在逻辑编程定理证明器 LPTP 中形式化证明 √2 无理性的过程。作者先定义基础逻辑程序谓词，再以自然演绎描述经典证明，并记录与 LLM 的交互，最终得到一份部分由模型生成、但经 LPTP 完整检查的形式证明。