AI 三天解出公开18年数学问题，两个形式化验证器通过

作者称，一个AI系统在三天内找到公开18年的数学问题证明，并经两个独立的软件形式化验证器逐步验证通过。作者据此指出，形式化验证可降低数学研究的试错成本，而在医学和工程等领域，候选方案仍受制于昂贵的真伪验证成本。