LeanTool

LeanTool 是将 LLM 与 Lean 编程语言/交互式定理证明器的「代码解释器」连接的简单工具；由于 Lean 近期快速演进，LLM 常难以输出正确的 Lean 4 语法，让其直接与 Lean 对话便能获得修正错误的机会。