Lean语言

我的 17 岁，是坐在教室里苦哈哈地刷数学卷子；而这个名叫 Enrique Barschkis 的高中生，利用课间休息时间，成功解决了困扰数学家多年的埃尔德什第 347 号问题。 这一成就不仅在社交平台 X 上引发热议，更得到了谷歌首席科学家 Jeff Dean 的盛赞。 什么是埃尔德什第 347 号问题？ 埃尔德什第 347 号问题，最初由埃尔德什和格雷厄…