On AI and Progress in Mathematics: Dreaming a Mathematical Universal Machine

In the autumn of 2026, mathematics is facing what may be the deepest crisis in its history. The entire ecosystem through which mathematical knowledge is produced, validated, communicated, and assessed is beginning to break down. Mathematics departments, those usually quiet and civilized places, are suddenly in turmoil -- the unlikely theaters of a new Battle of the Ancients and the Moderns. The source of the crisis is clear: AI systems have become better than even the best human mathematicians at proving and validating mathematical results. This document proposes a metaphor for mathematical activity: we once thought of ourselves as mountain climbers; soon, we may become miners digging in the mathematical mine, either collaborating or competing with mathematical AI machines. Publications would then be seen primarily as a means of helping humans understand mathematics, while the measurement of mathematical progress would be entrusted to a Mathematical Universal Machine. In nontechnical terms, we explore what this brave new world of mathematics might look like and how we might collectively shape its future.