Gary Marcus 批评 OpenAI 数学证明结果报告缺乏关键细节

Gary Marcus 在 X 上批评 OpenAI 发布的数学证明结果报告。他指出报告没有说明证明是一次生成后由 Lean 验证，还是经过迭代过程，也没披露失败率、训练与数据增强方法。Marcus 认为这种详细程度通不过同行评审，无法判断该结果能否泛化到数学之外，可能是通向 AGI 的一步，也可能只是 Lean 和合成数据在可验证领域里的巧妙应用。