MathCode是一款前沿数学编码智能体，形态是终端AI编码助手。它把自然语言描述的数学问题，转换成Lean 4定理，并自动完成形式化证明。对使用者来说，等于在终端环境里完成了“从题目到证明”的一整条链路。

从自然语言到可验证定理

打开网易新闻 查看精彩图片

数学题用自然语言写出来，存在歧义；Lean 4定理证明器则要求每个逻辑都精确。MathCode的定位就是跨越这道鸿沟：先把题目翻译成形式化定理陈述，再让证明过程自动化。

不只是证明：三类配套工具