李诞：有品位的数学家加公开的 GPT-6 Astra 强于 OpenAI 内部模型，但顶级数学家不愿用 lean4

李诞发文称，他相信有品位的顶级数学家配合公开的 GPT-6 Astra，胜过 OpenAI 内部没有品味的数学家加更强的超级内部模型。他指出问题是顶级数学家几乎没用过 lean4，许多人从内心认为这类 formal prover 是纯垃圾，不如大脑加手敲 latex。他表示年初向众人提起时，第一反应是被骂不懂 pure math。