2023年6月27日，加州理工学院和麻省理工学院研究者发表利用ChatGPT证明数学定理的论文，称数学的人工智能副驾驶（Copilot）时代已经到来，未来人工智能将能够发现数学定理。这篇论文构建了一个基于大语言模型（LLM）的定理证明器，为解决大语言模型幻觉方面的缺陷开辟了一条新途径。

研究人员提出一个开源平台LeanDojo，提供了用于数据提取和与Lean（证明助手工具）交互的工具；证明中的前提（现有定理）的细粒度标注；用于开发定理证明的机器学习模型——LeanDojo Benchmark；以及一个基于LLM的检索增强证明器——ReProver等工具包、基准和模型，为LLM创造了一种定理证明的交互式环境。

LeanDojo可从Lean中提炼出人类撰写的证明过程，形成一个数据集，从而通过与Lean的证明环境互动，使得这个训练出来的模型可以用来证明定理。实验显示，ReProver的性能优于Lean内置的证明自动化策略。

信息来源：

https://leandojo.org/

https://m.thepaper.cn/rss_newsDetail_23710932

https://mp.weixin.qq.com/s/paGPCdA97kryDmcsGmwyFg