Kevin Buzzard：50 条 Annals 定理用 Lean 形式化，4 位菲尔兹奖得主定理按字面陈述有误

Imperial College London 数学家 Kevin Buzzard 在 Machine Learning Street Talk 纪录片《Mathematics Just Changed Forever》中介绍，用 Lean 证明助手形式化《数学年刊》50 条定理时发现，4 位菲尔兹奖得主的定理按字面陈述是错的。