Terence Tao says AI crossed the formal verification threshold, but the readability bottleneck just got worse

当陶哲轩说AI跨过了数学形式化的临界点

Terence Tao reported that AI now completes formalization tasks in hours that previously took volunteers weeks, with Lean confirming correctness. But he also flagged that AI-generated proofs are verbose, poorly abstracted, and hard for humans to digest. The threshold crossed is 'proof is correct'; the new bottleneck is 'proof is usable.' An independent arXiv report documented the same pattern: a Claude Code proof passed Lean but an expert review found shortcuts and redundant definitions. Tao took three years to reach this judgment, and didn't back down even as dozens of mathematicians signed a 'Don't Believe the Hype' statement. The breakthrough is faster engineering on known paths, not AI discovering new theorems.

Why it matters: Three independent sources — Tao's original post, peer evaluation, and an arXiv report — not a media rehash. The two-layer breakdown of the 'threshold' is the article's core contribution, strong K axis. Deduction: it's a personal blog analysis, not a primary research release, a...