午夜#学术新闻#

自动证明形式化领域的新里程碑：

使用3万 LLM 词元将整本研究生数学教科书翻译成了 Lean 语言。

开源的、大规模的多智能体推理系统，而且确实有效
>蓝图+精益： http://t.cn/AXImuUUZ
>代码库+预印本： http://t.cn/AXM7pbCu

Darij Grinberg 的代数组合学导论（http://t.cn/AXImuUUz

以前是lean定理的证明，这次是验证教科书里的内容是无矛盾的。