小米 MiMo 2.6 Pro 协助完成李-约克定理 Lean 形式化，超 6000 行代码

bookwormengr · x · 2026-09-22

小米官方称，MiMo 2.6 Pro 协助研究人员完整形式化了李-约克经典论文《Period Three Implies Chaos》的原始主定理：在研究设计的探索策略引导下，多个 Subagents 协作完成定理表述与证明形式化，最终产出超 6000 行 Lean 4 代码，通过 Lean kernel 验证且无未完成证明占位符。值得注意的是 MiMo 2.6 Pro 并未针对 Lean 做专门后训练。发帖人借此预测：千禧年大奖难题的解答将来自多个实验室，而人们会因享乐适应很快将其视为平常。