MathCode

用 Lean 做形式化证明，查定理、试策略、看目标状态全靠手动来回切换。MathCode 是一个内置 Lean 能力的终端 AI 编码助手，可以检查证明目标、验证候选步骤、搜索声明，并交互式地验证完成的证明。

完整安装会带上 Lean 和 Mathlib，也提供不含 Lean 的精简安装方式。

软件功能

证明目标：查看当前待证目标。

候选验证：逐步检验证明策略。

声明搜索：在 Mathlib 中查找定理。

交互验证：确认完整证明是否成立。