「我預計，如果使用得當，到 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 推理，不限于定理證明。在本地或遠程運行任意模型（請參閱自帶模型）。

項目中還提到了一些高級用法，感興趣的讀者，可以去原項目了解更多內容。