陶哲轩：AI几周内跨过数学形式化临界点，证明生成快但审查跟不上

菲尔兹奖得主陶哲轩分享IEANTN项目体验，称自动形式化技术最近几周突然跨过某个临界点，过去需志愿者等数周才能认领的Lean形式化任务，现在AI数小时就能完成，待认领issue队列基本清空。