读到Marcus的博文我不同意陶哲轩，因为讨论的是我关心的话题，所以我想分享一下我的观点。
一、LEAN是可以接受的证明方法吗？
这个问题有一点点像“用AI写出来的程序可以接受吗”？
目前的共识应该是即使AI写出来的程序能跑，也应该有一个人类监视，避免它幻觉大发整出什么奇怪的bug。
LEAN给出的形式化证明并不天然是正确的。我知道有逻辑学家在力图证明LEAN的系统和当代数学使用的逻辑等价，但目前好像尚未有结果。目前来说，仅仅是给出LEAN语言证明并不能宣称它的逻辑是正确的。
（一部分）数学家认为LEAN给出的形式化证明作用是帮助人们理解某平替的证明，而非作为证明的替代。
二、AI可以判断命题的真假吗？
任何一个人类宣称自己证明了某结果，就必须公布自己的证明、进行同行审议后，此结果才会被认定为真，并且任何人随时都可以挑战此结果。
数学界有时也会出现某人给出的证明非常晦涩难懂，但结果重大，所以人们也会使用这个结果。但接下来的发展方向是：人们要么尝试给出该结果的另一种证明，要么找出另一种不使用该结果的证明。
没有理由AI的结果就自动享有认可。
三、我们应该用AI判断命题真假吗？
这个问题已经进入了社会学范畴。我个人觉得有两种视角。
站在数学家个人的视角上，应该使用AI辅助证明吗？
我个人觉得比起围棋这种游戏，数学更像是文学。在多大程度上我可以宣称我的工作是原创性的？目前我认为，AI的产出不算我的产出。即使退一步来说，我使用了AI，我也应该对我的内容里的每一个细节了若指掌。
可是，当人有了捷径要走，人真的能去下苦功夫搞明白每一个细节吗？
站在社会的角度上，应该使用AI证明数学命题吗？
这个问题回到第二点，目前AI的可信度尚未得到认证。我还是认为接受AI的证明和接受随机某个人类的证明不应该有区别。
四、我不是数学家，所有的定理对我来说都是黑盒子，凭什么数学家可以代表人类反对AI？
我觉得陶哲轩那个药学的例子很好，但他搞错了重点。重点其实应该是“临床试验”。如果AI宣称发现了某种癌症新药，那么你会直接相信它、直接开始生产吗？不会吧？在那之前还是需要人类去做临床试验，验证它的宣称吧？
而且在做临床试验之前——因为这可是很大一笔投入——也需要有人类先去验证AI的宣称，试图去理解它在说什么，看看到底有多少可行性吧？
“我不理解无所谓”，不能推出“没有人理解也无所谓”。“我不理解也无所谓”是因为有人去做了理解、验证的工作。
那为什么这些“有人”有信誉？科学家的信誉是建立在可复现的基础上。不是某个数学家代替了全人类去验证知识真伪，而是一群数学家交互验证。
说到底，这又回到第二点。AI给出了一种证明，现在需要有人去验证，否则它的结果就没有信誉。
（而且说真的，AI在可信度这方面的信誉不是一直在破产吗？）
五、最后发散一下
我很认同人类数学家协会的观点，OpenAI一次性抛出这么多（烂得惨绝人寰的）证明，并不是为了增加人类的知识，而是在展示自己的肌肉。
它并没有付出多大精力来让人类理解它的证明（我不相信大语言生产模型只能写出这么烂的英语），老实说我会想：那干脆人类也别去理解，直接当它不存在好了！
但是数学家并不是它想impress的对象，那些手里拿着钞票的人大概率不会真的去读这些（狗屁倒灶的）论文。很可惜，现在的世界就是这样运转的。
最后说说数学之美。数学之美的前置条件是“真”，在那之后才谈得上什么形式美。数学家负责数学之美的第一条就是判断真伪。