Terence Tao draws an extended analogy between the impact of AI and formal proof tools on mathematics and the impact of the automobile on cities. Just as cars enabled faster travel but degraded walkable urban communities, AI can generate proofs more efficiently but strips away the secondary benefits of human mathematical work: skill development, narrative, pedagogical insight, and discovery of unexpected terrain. Rather than forcing AI into existing human-oriented infrastructure or simply making AI more powerful, Tao argues for building new 'machine-friendly' mathematical infrastructure — such as large-scale curated challenge problems verified by proof assistants, or automated low-quality proof libraries that humans then refine. He warns against destroying the 'walkable' nature of mathematics and suggests a new discipline of 'AI planning' may be needed. Replies push back on the analogy's limits and call for mathematicians to focus on formal, objective analysis of AI rather than societal speculation.
Sort: