陶哲軒採用大型模型的證明助手Lean，展現其偏好

「我預計，如果使用得當，到 2026 年，AI 將成為數學研究和許多其他領域值得信賴的合著者。」數學家陶哲軒在之前的一篇部落格中說道。

陶哲軒這樣說了，也這麼做了。

他最近一直在用 GPT-4、Copilot、Lean 等工具進行數學研究，並且還在 AI 的幫助下發現了自己論文中的一處隱藏 bug。

最近，陶哲軒表示Lean4計畫已經成功完成了多項式Freiman-Ruzsa 猜想（PFR）的證明的形式化，僅耗時三週。同時，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來實現證明自動化，包括策略建議、前提和搜尋證明

使用者可以選擇使用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 在數學上的性能。

Copilot的效果示範

#大家可以依照官方教學來設定Lean Copilot，配置完成之後就可以開始實驗了。專案的作者也提供了一些官方範例供參考

#推薦方案。匯入LeanCopilot後，您可以使用suggest_tactics產生推薦方案。在使用過程中，您也可以點擊推薦方案，並在證明中使用它（參考下圖）

#你可以使用前綴，例如simp，來限制生成的策略

搜尋證明。使用search_proof將LLM產生的策略與aesop（Lean 4的白盒自動化專案）結合起來，以搜尋多個策略證明。找到證明後，您可以單擊該策略將其插入編輯器中

#重寫後的內容：選擇前提是一項重要策略。該策略的目的是檢索一份潛在有用前提的清單。目前，Lean Copilot會利用LeanDojo中的檢索工具，從Lean和mathlib4（即Lean 4數學庫）的固定快照中選擇前提

#您可以執行LLM。無論是定理證明還是其他推理，都可以在Lean中運行LLM。您可以在本機或遠端執行任何模型（請參閱自帶模型）

#專案中也提到了一些進階用法，有興趣的讀者，可以去原項目了解更多內容。

以上是陶哲軒採用大型模型的證明助手Lean，展現其偏好的詳細內容。更多資訊請關注PHP中文網其他相關文章！