现在，数学辅助注明东西都用上了大模型。
「我预计，如果利用得当，到 2026 年，AI 将成为数学钻研和许多其他领域值得信赖的合著者。」数学家陶哲轩在之前的一篇博客中说道。
陶哲轩这样说了，也这样做了。
他最近一直在用 GPT-4、Copilot、Lean 等东西从事数学钻研，并且还在 AI 的帮助下发现了自己论文中的一处隐藏 bug。
不仅如此，前几天，陶哲轩表示：对多项式 Freiman-Ruzsa 想象（PFR）的注明从事形式化的 Lean4 项目成功完成，并且耗时仅三周时间。Lean 编译器也报告该想象符合标准公理，可以说这是计算机和 AI 辅助注明的一项巨大成功。
关于上述钻研的更多内容，感兴趣的读者可以参照《陶哲轩用 AI 形式化的注明究竟是什么？一文看懂 PFR 想象的前世今生》。
看到这，细心的读者可能已经发现了端倪，陶大神在从事数学钻研时，多次都提到过 Lean。简单来讲，Lean 是一种可帮助数学家考证定理的编程语言，用户可以在其中编写和考证注明。相比初代 Lean，现在最新的 Lean 4 版本从事了多项优化，包括更快的编译器、改进的错误处理和更好的与外部东西集成的能力等。
在数学领域被广泛利用的 Lean，在大模型（LLM）刷屏的今天，两者有没有更好的结合方式呢？
现在已经有人实现了，开放平台 LeanDojo 团队（关于 LeanDojo，可参照「AI 大模型帮陶哲轩解题，还能注明数学定理了？」）和加州理工学院的钻研者推出了 Lean Copilot，这是一款专为 LLM 与人类交互而设计的协调东西，旨在通过人机协调给出 100% 准确的形式化数学注明。
值得注意的是，LeanDojo 团队的钻研主要集中在利用 LLM 自动化定理注明方面，从这点也不难看出，他们推出的 Lean Copilot 和 LLM 相关也不会令人吃惊。
项目地址：https://github.com/lean-dojo/LeanCopilot
对于这项钻研，大家除了说 Cool，就是 very cool，评价还是很高的。
在 Lean 中利用 LLM，加快数学注明速度
一直以来，自动化定理注明面临重重困难，传统上，数学注明依赖于手工推导，需要细致的考证。现在随着 AI 的进步，钻研者开始借助人工智能从事深入探索，但又免不了出现这种问题，即 LLM 在数学和推理任务中有时不是很靠谱，容易出现错误和幻觉。
Lean Copilot 允许用户在 Lean 中利用大型语言模型来自动化注明过程，从而显着加快注明合成的速度，在必要时还允许人类无缝介入和修改，从而在机器和人类智力之间提供平衡的协调。
Lean Copilot 允许在 Lean 中利用 LLM 来使注明自动化，如战略倡议（suggesting tactics）、条件（premises）以及搜寻注明（searching for proofs）。
用户可以采用利用 LeanDojo 提供的内置模型，或者导入自己的模型。这些模型可以在内地运转（无论是否有 GPU），或者在云端运转。
简而言之，Lean Copilot 为用户提供了一个灵活的方式，通过引入 LLM 来增强和优化在 Lean 中从事定理注明的过程。
Lean Copilot 的主要特点可总结为：
LLM 能够提出注明步骤，搜寻注明，并从大型数学库中采用有用的引理。
Lean Copilot 可作为 Lean 包从事设置，并且能够无缝地在 Lean 的 VS Code 工作流中运转。
用户可以利用 LeanDojo 中的内置模型，或者利用自己的模型，这些模型可以在内地（有或没有 GPU）或云端运转。
该东西可在各种平台上运转，包括 Linux、macOS 和 Windows WSL。
为了使 LLM 更易于 Lean 用户利用，Lean Copilot 希望能够启动一个正反馈循环：注明自动化将带来更好的数据，并最终提高 LLM 在数学上的性能。
Lean Copilot 效果展示
大家可以根据官方教程配置 Lean Copilot，配置好后就可以从事实验了。项目作者也给出了一些官方示例。
战略倡议。导入 LeanCopilot 后，你可以利用 suggest_tactics 生成战略倡议。利用过程中，你也可以点击倡议的战略，并在注明中利用它（参照下图）。
你可以提供一个前缀如 simp 来约束生成的战略。
注明搜寻。如下图所示 search_proof 将 LLM 生成的战略与 aesop （用于 Lean 4 的白盒自动化项目）相结合，来搜寻多战略注明。找到注明后，你可以单击该战略以将其插入编辑器中。
条件采用。该战略用于检索潜在有用条件（premises）的列表。目前，Lean Copilot 利用 LeanDojo 中的检索器从 Lean 和 mathlib4 （Lean 4 数学库）的固定 snapshot 中采用条件。
运转 LLM。你还可以运转 Lean 中的任何 LLM 推理，不限于定理注明。在内地或远程运转任意模型（请参阅自带模型）。
项目中还提到了一些高级用法，感兴趣的读者，可以去原项目了解更多内容。
参照链接：https://analyticsindiamag.com/lean-co-pilot-lets-you-use-llms-as-copilots-in-lean/