Math-AI推出MathCode：将日常语言问题转为Lean 4定理并尝试证明

RecodeX 重构消息，一个与普林斯顿研究员Yifan Zhang相关的开源研究社区Math-AI，近日发布本地终端助手MathCode。该工具可将自然语言问题转换为Lean 4定理并尝试形式化证明，同时存储和复用已成功证明的定理。