观点：数学界的“存在危机”源于 Lean 跨过临界点，而非 AI

idanbeck 提出，数学界当前面临的所谓“存在危机”，更可能源于 Lean 跨过某个临界成熟度，而非 AI 带来的冲击。这一判断将讨论焦点从“AI 取代数学家”转向形式化验证工具生态的长期积累及其与数学共同体的紧张关系。