Lean 4 最劝退人的地方，很多时候不是数学本身。
是你已经知道一个命题对。
比如偶数的平方还是偶数。
脑子里两行就过了，真写到 Lean 里，先卡在定理怎么声明。变量怎么放，类型怎么写，Nat 还是 Int，Mathlib 里有没有现成引理，编译器又在报哪一行。
证明还没动手，人已经有点烦了。
MathCode 盯的就是这段。
它不是让你自己写好 Lean，再让模型补几句 tactic。它的入口更粗暴一点：直接给一句自然语言数学问题，它先转成 Lean 4 的 formal statement，再接着试证明。
像“证明偶数的平方是偶数”。
你扔进去，它往 Lean 那边翻。
翻完还不算结束。
MathCode 会调 Lean LSP，看编译反馈；会去 Mathlib 里找可能用得上的引理；证明跑不过，就继续改。项目里写的是最多可以迭代 10 轮。
这个地方我会多看两眼。
很多 AI 定理证明工具，演示页都挺漂亮。真用的时候，模型吐出一段 Lean，编译一跑，红一片。然后剩下的活还是你自己来：查库，改 tactic，猜类型，继续撞墙。
MathCode 至少没有假装“生成完就完事”。
它把报错修复也放进了流程里。
还有一个点，它不是只押一条证明路线。
项目支持多个 planner 并行跑，几条思路一起试。哪条能走通，哪条更短，再往后挑。
这倒很像人做题。
不是一上来就神乎其神地写出证明，而是先拆一下，试一下，不行换招。数学证明很多时候就是这样，不体面，但真实。
我反而觉得，这比“模型秒证定理”那种说法可信一点。
还有个偏笔记向的功能：生成 Obsidian 知识图谱。
定理、引理、依赖关系拉出来，看着会清楚一些。尤其是 Lean 这种东西，证明一长，前面用了哪个 lemma，后面又绕到哪里，很容易散。
图谱不一定天天用。
但复盘的时候有用。
当然，别把 MathCode 想成一句话许愿机。
自然语言本来就含糊。Lean 又不吃含糊。命题稍微复杂一点，形式化声明可能就要改；Mathlib 里引理找得到，不代表用得上；自动修十轮，也可能十轮全红。
这很正常。
它更像是把门槛往下压了一截。
原来你要自己在终端、Lean 4、Mathlib、报错信息之间来回切。现在 MathCode 试着把这些东西塞成一个流程。能不能全自动另说，至少不用一开始就被那些碎活劝退。
我对它的判断也比较简单：不是替你会数学。
是先替你少烦一会儿。
GitHub 地址： https://github.com/math-ai-org/mathcode