这些数学问题是不是有足够的算力就能解决？以前解决不了是因为算力不够

seed还不算顶尖吗，卡多人也多，成果也不少吧，很强的

这个和模型的算力联系不大，那些常用的大模型参数都够的甚至是过剩。主要看建模，数学家如何去把复杂问题分解，然后丢给agents。现在大模型数据量很强是一方面，强大的建模和agents才能最大发挥数据的能力。

和王虹合著菲奖论文的约书亚扎尔就是南开聘请的教授啊

lean形式化证明本身难度就不是很高，主要是工作量巨大，所以正适合AI去做，但体现不出来太多推理能力

其实这次有争议的就是openai是否剽窃人类的计算方式吧

难道说？！

这不是形式化证明，这是形式化验证，是在已有证明的基础上，把证明翻译成lean