交互工具¶

如何与 Lean 进行交互，并与大语言模型结合是当前的一个热门话题。目前社区已存在丰富的工具生态，包括：

• LeanDojo - Lean 交互式证明助手
• REPL - Lean 官方交互式环境
• Pantograph - 为支持机器学习应用场景开发等 Lean4 交互工具
• lean-repl-py - REPL 的 Python 封装
• itp-interface - 多语言的交互式定理证明接口
• leanclient - 基于 Lean 语言服务器的交互工具

当前文档提供了部分工具的使用教程，欢迎补充和完善。