定理证明

连接自然语言推理与 Lean 机器验证：Infoview 反馈、Mathlib 导航、MCP 补全与可读性解释。

演示视频

核心能力

• 在 Markdown 中陈述问题，智能体写回自然语言证明。
• 将陈述与证明形式化为 Lean，在线编译并实时查看 Infoview。
• 悬浮信息、Go to Definition 跳转 Mathlib、自然语言定理搜索。
• 智能体读取编译器反馈，持续修改与补全证明。
• 选中 Lean 片段请求自然语言解释，可写回 TeX 或 Markdown。

开始使用

• Lean 形式化指南