菲尔兹奖得主陶哲轩当众警告：AI正在量产“没有人类能看懂”的数学证明，整个学科面临史诗级消化不良

TL;DR - A WeChat write-up of Terence Tao's ICM 2026 lecture "Mathematics in the Age of AI," where he warns that AI can now mass-produce research-level proofs cheaply, creating "proof indigestion" because human verification, exposition, and assimilation cannot keep pace. It matters because it reframes the bottleneck of AI-accelerated science from generation to human understanding.

• Tao splits a proof's lifecycle into six stages — generation, verification, exposition, publication, digestion, canonization — arguing AI plus formal tools (e.g., Lean) accelerate only the first two while the remaining four congest.
• Cited evidence: the First Proof project reported 7 of 10 novel research-level problems solved to publishable quality by at least one team, at $10–$1,000 per problem; erdosproblems.com is reportedly accumulating AI-submitted proofs without enough qualified volunteer verifiers.
• He invokes Goodhart's law (optimizing "solve more problems" diverges from understanding/teaching), notes AI-polished text erases the "friction" that signals hard steps, and observes long correct proofs are easier to generate than short elegant ones.
• Three prescriptions: normalize disclosure of AI assistance; reward refereeing, surveys, and translation of machine proofs over priority races; and a "talk test" — if authors cannot give a clear, expert-level, correctly attributed talk on a result, it should not be published.