Lean 代码交互方案

发表于 更新于 阅读次数： 字数： 417 时间 ≈ 2 分钟
TODO

与 Lean 代码进行交互的几种方案：

  1. 在命令行运行 Lean 文件。

  2. 在 Lean 内部运行元编程的策略。

  3. 使用 Lean 的语言服务器进行代码交互：可能会比较复杂，且存在硬编码的延迟。

  4. 由于 Lean 本身是 Lean 编写的：可以重用 Lean 的解析器、内核或解释器，进行更高效的交互。（需要精通 Lean 的开发，大概就 DeepMind 团队能做到）

目前与 Lean 环境交互相关的项目：

  1. 社区维护的 REPL 项目，通过命令行输出 JSON 交互
  2. 基于 REPL 项目开发的 lean4_jupyter：
    20241128102900
  3. 前端项目：运行 Lean 代码的 lean4web，运行 Lean 游戏的 lean4game，运行 Lean 的 Vscode 插件 vscode-lean4
  4. 代码解析和交互工具 LeanDojo
  5. 基于 LeanDojo 的证明搜索工具 LeanCopilot：
    20241128103514
  6. 定理可视化工具：ProofWidgets4
    20241128100229
  7. 自然语言语句转 Lean 代码的 LeanAide：
    lean-aide-example
  8. 证明搜索工具 llmstep：
    llmstep

此外 12月中旬 NeurIPS 数学研讨会 的报告：ABEL: Sample Efficient Online Reinforcement Learning for Neural Theorem Proving。作者基于 Aesop 开发了一个 REPL，后续将开源。Math-AI 讨论会其他研究也值得留意。

REPL

1
2
3
4
git clone https://github.com/utensil/lean4_jupyter.git
cd lean4_jupyter
pip install .
-m lean4_jupyter.install --user