消耗1830亿token，Meta用AI把数学教材翻译成了一个超大Lean库|meta|定理|教科书|数学教材|数论|翻译_手机网易网

翻译,定理,数论,教科书,meta,数学教材

编辑｜Panda数学正在迎来AI革命。最近几个月尤为明显。比如，就在前几天，GoogleDeepMind新论文宣布其最新系统AlphaProofNexus在一次自主运行中，解决了353道开放Erdős问题中的9道，其中两道已在数学界悬而未决长达56年，并且每道题的推理成本，仅需区区几百美元。