专题：ai-math

团队在“First Proof”数学挑战中首次提交了基于大语言模型的自动证明实验。通过微调 GPT‑4‑Turbo 并使用链式思考提示，模型在 10 条高阶定理中生成了 3 份形式化草稿，其中 1 份在 Coq 中通过基本检查。实验展示了模型在推理速度上的优势，但在逻辑严谨性和跨领域概念掌握上仍有显著不足，后续将引入交互式定理证明器进行闭环优化。