新华社客户端天津9月8日电（记者张建新、栗雅婷）近日，南开大学陈省身数学研究所讲席教授郭少明带领团队与字节跳动Seed合作完成三维粘性挂谷猜想的形式化验证工作，并在开源代码托管平台GitHub上发布。这一成果实现了对现代数学领域重要成果的一次机器形式化验证，也为未来利用计算机处理更大规模、更复杂的数学证明任务提供了重要实践。
形式化验证是对数学证明使用计算机进行精准的验证。传统数学证明的验证依靠人工进行，时间周期较长。而形式化验证能做到逐逻辑推演核对证明过程，让数学结论在短时间内得到更广泛的认可。
此次形式化工作总共完成约180万行Lean代码的书写，其中约90%由字节跳动Seed团队研发的Seed-Prover完成。数学方面的工作及部分代码由郭少明带领团队成员陈铭峰、庞逸轩和沈敏行完成。
南开大学陈省身数学研究所由“整体微分几何之父”陈省身于1985年在母校南开大学创立，他希望为在数学方面愿意潜心研究的人创造一个适宜的环境，让青年人尽早地懂得欣赏“好的数学”。1986年，诺贝尔奖获得者杨振宁在所内建立理论物理研究室，为该所奠定了坚实的国际学术基础。自建所以来，研究所始终秉持“立足南开，面向全国，放眼世界”的宗旨，着力在本土培养数学人才，邀请世界一流数学家来校讲学，举办一系列国际学术会议，为南开数学在全国乃至世界赢得了盛誉。（完）
原文链接：南开大学与字节跳动完成三维粘性挂谷猜想形式化验证
审核：韦承金
|
