【新智元导读】重磅！大语言模型在定理证明领域展现惊人实力，引领数学研究新潮流。这项由加州理工华人领衔的研究团队所取得的突破，正逐步改变数学的未来。
近日，数学界迎来一项重大科技进展，引起了广泛关注。由加州理工、英伟达等机构学者共同研发的一个基于开源LLM的定理证明器，正以前所未有的速度推进数学的进步。这一重要成果得益于大语言模型（LLM）的强大能力，使得计算机能够理解和证明数学定理，展现出人工智能的惊人潜力。
著名的数学家陶哲轩曾预测，到2026年，AI将结合搜索和符号数学工具，成为数学研究中不可或缺的合作者。如今，这一预测正在逐步成真。
该项目以LeanDojo为平台，提供了一个定理证明的交互式环境，配备了工具包、基准和模型。其独特的严格评价系统，通过代码生成的方式进行定理证明，有效避免了模型产生幻觉的可能性。这一创新之处为解决LLM在事实性和幻觉方面的问题开辟了新的途径，标志着人工智能在数学领域的首次重大突破。
论文第一作者杨凯峪强调，公式证明是一种可验证正确性的计算机程序。更重要的是，这项研究为解决LLM在事实性和幻觉方面的缺陷提供了新的思路。定理证明过程的严格性和可验证性为解决LLM问题提供了一个全新的视角。
英伟达首席科学家Jim Fan对此表示赞同，并指出数学的飞速发展将带领人类进入一个前所未有的新世界。他认为，数学的独特性质使得它成为人工智能发展的理想领域。与其他需要物理实验的学科相比，数学的发展几乎不受物理条件的限制。
随着人工智能技术的发展，尤其是大型语言模型的不断进步，定理证明领域的前景日益广阔。LeanDojo通过与Lean证明助手的紧密集成、丰富数据集以及强大的机器学习模型，为数学家提供了一个强大的定理证明工具。它能够提取人类撰写的证明过程，并通过与Lean的证明环境互动，使训练出的模型能够证明定理。LeanDojo还提供了丰富的环境和工具，方便数学家们观察证明状态、运行策略、接收反馈等。这对于评估和改进证明器以及通过强化学习进行训练至关重要。该工具还能发现一些定理的新证明方法和公式的错误，展示了人工智能在数学领域的巨大潜力。
这一突破引起了广大网友的关注和讨论，人们纷纷表示对人工智能在数学领域的未来发展充满期待。这项研究不仅标志着人工智能技术在数学领域的巨大潜力正在逐步被发掘和实现，更是对人类智慧的一次重大挑战和超越。让我们共同期待这一领域的更多精彩发展吧！
