谷歌DeepMind开源首个形式化数学猜想库，获菲尔兹奖得主陶哲轩力挺

谷歌DeepMind开源了首个形式化数学猜想库，通过将数学猜想转化为计算机可读的形式化语言，助力AI破解数学难题。该项目得到了菲尔兹奖得主陶哲轩的高度认可，目前已收录解析数论中的4个兰道猜想等重要问题，并面向全球数学家征集更多猜想。形式化语言能够避免AI因模糊表述而产生无意义答案，从而提升解决问题的有效性。此外，该数据库不仅为自动定理证明器提供了优质基准测试集，还通过扩展mathlib促进了数学工具的发展。项目支持多种形式化贡献，涵盖新增问题、需求提交及错误修正等，旨在打造一个不断扩展的数学宝库。
来源：https://mp.weixin.qq.com/s/OWjLg4pipboQGU-u4KN71w