LeanCopilot

收录理由

Lean Copilot 把大模型的能力直接嵌进 Lean 的证明环境里，写证明时不用切到聊天窗口，就能在编辑器里拿到建议。它能根据当前证明状态推荐下一步 tactic，从 mathlib 里挑出相关的 premise，还能自动搜索完整的证明过程。项目自带 LeanDojo 的预训练模型，也支持接入你自己跑的模型，无论是本地还是云端，这对于需要自己控制硬件或在意隐私的团队来说很实用。因为它是 Lean 原生的包，只要在 lakefile 里加个依赖，就能在证明内部调用它的 API。对于用 Lean 做形式化数学的团队，这是一个能加快证明开发速度、同时又不放弃模型掌控权的实际工具。