“I therefore disagree with claims that mathematics is over because machines can prove theorems.”
A Lean proof can run to hundreds of thousands of lines that nobody can read. OpenAI threw 4,000 problems at a model and solved “some hundreds”, and that got reported as a breakthrough. The real ask here is buried at the end. Universities should run their own models instead of renting from three companies that decide which problems matter.