AI's potential to lower the cost of mathematical proofs

A post on AI and theoretical computer science argues that the field had defensible reasons to celebrate problem-solving: important proofs often signaled creativity, persistence and deep understanding. But it predicts that AI tools could prove many theorems quickly, dramatically reducing the cost of obtaining proofs for well-posed mathematical questions. The scarce intellectual work, it suggests, would then likely shift toward formulating questions, models, theories, definitions and conjectures.