文章预览
Datawhale分享 最新:陶哲轩,编辑:新智元 AI,已成为菲尔兹奖得主最得心应手的工具。 大约三周前,陶哲轩提出了一个协作项目—— 结合专业和业余数学家、自动定理证明器、AI工具,以及证明辅助语言Lean,来描述与4694条幺半群(magmas)方程定理定理相关的蕴含图。 这些定理最多可以使用,四次幺半群运算来表达。 也就是说,需要确定4694条定理之间可能存在4694 * (4694 - 1) = 22028942蕴含的关系真伪。 地址:https://github.com/teorth/equational_theories/blob/main/data/equations.txt 这一项目在9月25日发布当天便启动了,如今,已经紧锣密鼓进行了19天。 刚刚,陶哲轩公布了项目的最新进展: 从已解决原始蕴含关系角度来看,截至目前,项目进度已完成99.9963%。 在需要解决的22028942个蕴含关系中,8178279个被证明为真,13854531个被证明为假,只有826个仍未解决。 而
………………………………