標籤 Lean

2026 年 10 月 27 日上架的 Lex Fridman 第 503 集緊急對談，邀 Brunton、Moitra、Kontorovich 三位數學家回應機器證明潮。本文對照官方逐字稿與 OpenAI、Clay、Lean、Anthropic、陶哲軒等原始文件，拆解證明被接受的三層驗收：推導正確、題目對齊、方法可遷移，以及制度怎麼接住最難自動化的理解工作。