【儀表網(wǎng) 研發(fā)快訊】近日，南開大學陳省身數(shù)學研究所講席教授郭少明帶領團隊與字節(jié)跳動Seed合作完成三維粘性掛谷猜想的形式化驗證工作，并在開源代碼托管平臺GitHub上發(fā)布。這一成果實現(xiàn)了對現(xiàn)代數(shù)學領域重要成果的一次機器形式化驗證，也為未來利用計算機處理更大規(guī)模、更復雜的數(shù)學證明任務提供了重要實踐。
 

　　形式化驗證是對數(shù)學證明使用計算機進行精準的驗證。傳統(tǒng)數(shù)學證明的驗證依靠人工進行，時間周期較長。而形式化驗證能做到逐邏輯推演核對證明過程，讓數(shù)學結(jié)論在短時間內(nèi)得到更廣泛的認可。
 

　　此次形式化工作總共完成約180萬行Lean代碼的書寫，其中約90%由字節(jié)跳動Seed團隊研發(fā)的Seed-Prover完成。數(shù)學方面的工作及部分代碼由郭少明帶領團隊成員陳銘峰、龐逸軒和沈敏行完成。
 

　　南開大學陳省身數(shù)學研究所由“整體微分幾何之父”陳省身于1985年在母校南開大學創(chuàng)立，他希望為在數(shù)學方面愿意潛心研究的人創(chuàng)造一個適宜的環(huán)境，讓青年人盡早地懂得欣賞“好的數(shù)學”。1986年，諾貝爾獎獲得者楊振寧在所內(nèi)建立理論物理研究室，為該所奠定了堅實的國際學術(shù)基礎。自建所以來，研究所始終秉持“立足南開，面向全國，放眼世界”的宗旨，著力在本土培養(yǎng)數(shù)學人才，邀請世界一流數(shù)學家來校講學，舉辦一系列國際學術(shù)會議，為南開數(shù)學在全國乃至世界贏得了盛譽。
 

　　引用：南開大學與字節(jié)跳動完成三維粘性掛谷猜想形式化驗證-媒體南開-南開大學【引用時間：2026年9月10日】