证明氛围的时代已经来临。 来自 @HarmonicMath 的亚里士多德被用于在 @leanprover 中形式化陶哲轩对厄尔多斯问题的证明。 我们开始看到 AI 在新的数学发现中发挥重要作用。当与形式验证结合时，我们将不再需要人类来审查和检查证明的有效性，这将使飞轮转动得更快，并大大加速前沿的进展。