数学家沦为 AI 证明的免费审核工?Lean 圈争论引热议

turincomplete · x · 2026-10-10

在一场关于 AI 生成数学结果的讨论中，网友 @turincomplete 用反讽口吻抱怨：数学家如今不得不从事繁重劳动去验证 AI 批量产出的（slop）证明结果，还"理应感恩"数十亿算力建设、数万亿融资和市值的投入。

回复者 @suchenzang（AI 研究者）调侃这是"免费的社区 Lean 苦力被开采"。讨论触及 AI 圈真实矛盾：AI 辅助数学证明越来越强，但形式化验证（Lean）的重担落在了人类数学家身上。