Lean4

面壁智能让 AI 学会翻译数学命题 — 中国 AI 公司开始啃硬技术

自动形式化是让 AI 把数学命题翻译成机器能验的代码。面壁智能这周开源 MathForm 和 36.7 万条数据集，把这条流水线从手工活做成自动化。背后信号：中国 AI 公司正从拼参数转向啃工程深度。