OpenAI 求解数学题引发学界的非技术性思考

OpenAI 模型解决数学难题引发了关于证明可靠性及数学未来走向的讨论。作者反思了 Lean 形式化验证中可能存在的编码偏差与人工复核的必要性，并指出当前 AI 更多是结合已知思路而非提出全新范式。文中进一步探讨了 AI 生成证明对学术署名、人才培养及商业模式的潜在冲击，认为即便 AI 能解决部分问题，人类在可读性展示和新问题发现上仍具不可替代的价值。