中新网天津9月12日电(记者 孙玲玲)近日，南开大学讲席教授郭少明带领团队与字节跳动Seed合作完成三维粘性挂谷猜想的形式化验证工作，并在开源代码托管平台GitHub上发布。
据悉，这一成果实现了对现代数学领域三维挂谷猜想的一次机器形式化验证，也为未来利用计算机处理更大规模、更复杂的数学证明任务提供了重要实践。
形式化验证，简单说就是对数学证明使用计算机进行精准的验证。传统数学证明的验证依靠人工进行，时间周期较长。而形式化验证能做到让数学结论在短时间内得到更广泛的认可。
三维挂谷猜想是现代数学中的著名难题之一，最终于2022年至2025年由王虹和约书亚·扎尔在三篇文章所证明。据介绍，此次形式化验证的三维粘性挂谷猜想在他们的前两篇文章中证明，同时也是他们最后一篇所需要依赖的关键结果。
此次形式化工作总共完成约180万行Lean代码的书写，其中约90%由字节Seed团队研发的Seed-Prover完成。Seed-Prover使用了Seed-Evolving作为模型底座，采用Agent-Team的方式进行大规模并发形式化。数学方面的工作及部分代码由郭少明教授带领团队成员陈铭峰、庞逸轩和沈敏行完成。
当前，基础数学是人工智能大模型迭代升级、核心算法突破、推理能力跃升的底层支撑，数智交叉融合已成为前沿科技攻关与产业创新的核心方向之一。前不久，南开大学陈省身数学研究所、数学科学学院与字节跳动正式签约，共同成立“数学与智能联合实验室”，深化数学基础研究与人工智能前沿领域交叉创新，打造产学研深度融合的高水平协同创新平台。
据悉，南开大学与字节跳动将依托各自在基础数学研究与人工智能技术应用领域的优势，围绕人工智能与数学交叉融合开展深度合作，推动数学科研工具创新与大模型推理能力提升。此外，联合实验室还将在人才培养等方面开展全方位合作，努力打造数学与人工智能交叉领域的重要创新平台。(完)
进口增速快于出口，中国大市场澎湃全球新机遇
延续强劲增势 中国外贸交出优质“三季报”
一碗川渝酸辣粉，如何让河南小城长出百亿产值？
向海而生 向新而行｜天津，正在“更新”
高超音速导弹有多难拦截，沙特的遭遇很能说明问题
人这一辈子，一定要自驾一次阿禾公路看秋天！
美国该制裁自己了
埃塞前总统穆拉图·特肖梅：“中国的环境某种程度上塑造了我”
台湾网红柳杰克：台湾就是中国一个省！
人这一辈子，一定要去一趟长征集结出发地！
地面战斗白热化，胡塞武装围困上万也门政府军
中新网评：“不烧心”火了，别让“良心”凉了
红绿古交相辉映 赣鄱大地气象新
远视储备不足，近视还有多远？
郑钦文谈“低谷期”：这不一定是坏事，总有回来的时候
第二十六届工博会：“智”造业东风吹更劲
人这一辈子，一定要去一趟马鞍山：一半是铁水奔流，一半是诗仙明月
从博洛尼亚拱廊到隋唐洛阳城，古城保护理念为何共通？
白雪落黑土：黑龙江秋耕收尾蓄力来年丰收
近千名学子探秘平陆运河 感受中国基建力量
首列“京铁燕赵班列·助汇冀黔号”开行
人形机器人上岗工厂车间 企业两到三年可“回本”
山东枣庄：粉黛乱子草进入盛花期 粉色花海如云似霞