AI has made proving theorems cheaper than understanding them
Mathematics used to rely on scarce, difficult theorems as a rough signal that someone had developed real understanding. Bryna Kra argues that AI is breaking that signal: models can now produce polished proofs, including attacks on long-standing problems such as the Nivat conjecture, faster than experts can verify and absorb them. The bottleneck is shifting from discovery to deciding which machine-made results deserve trust and attention.