北京
数学证明历来是耗时费力的脑力劳动。如今，一款名为 MathCode 的终端 AI 编程助手，试图把“用自然语言描述一个数学问题”直接变成“Lean 4 定理并自动完成形式化证明”。 MathCode 内置了数学形式化引擎，你只需用日常语言输入题目，它就会自动转换为 Lean 4 定理，并启动交互式证明。它不仅仅是一个翻译工具，更像一个工程师：持续读取编译错误、修正思路、重新编译，直到证明通过。 最直观的飞跃是速度。传统 Lean 编译一次往往需要等待约 30 秒，而 MathCode 通过常驻的 Lean REPL，经过一次性预热后，将编译检查压缩到约 0.4 秒。这意味着，你可以在几分钟内迭代数十次证明策略，而不是在等待中消磨耐心。 除了速度，MathCode 还提供了系统化的知识管理： - 每个证明都会自动命名、存储并成为可导入的定理，供后续复用。 - 对话中的假设会被固化为持久化的、经过一致性检查的 Lean 声明。 - 自动检索 leansearch.net 和 Loogle，快速找到已验证的 Mathlib 引理。 - 生成 Obsidian 知识库，将定理与引理之间的依赖关系可视化为知识图谱。 - 支持将复杂定理拆分为多个独立子目标，并行证明后再拼接。 - 并行运行多个规划器，探索不同的证明路径，让证明器挑选最优策略。 安装方式也相当简单（需要 macOS arm64 或 Linux x86_64，以及 codex CLI）： git clone https://github.com/math-ai-org/mathcode.git cd mathcode bash setup.sh codex auth login mathcode 试着运行： mathcode -p "prove that the square of an even number is even" 输出将写入 LeanFormalizations/ 目录；也可用 ./run webui 启动浏览器界面。 如果你在研究中使用 MathCode，可引用以下论文： @misc{mathcode2026, title = {MathCode: A Frontier Mathematical Coding Agent}, author = {Team Math-AI}, journal = {math-ai-org.github.io}, year = {2026}, month = {April}, url = {https://github.com/math-ai-org/mathcode} } 数学证明可能永远无法完全自动化，但 MathCode 让它不再像一场漫长的苦役。
特别声明：以上内容(如有图片或视频亦包括在内)为自媒体平台“网易号”用户上传并发布，本平台仅提供信息存储服务。
Notice: The content above (including the pictures and videos if any) is uploaded and posted by a user of NetEase Hao, which is a social media platform and only provides information storage services.
