Nel giro di quattro giorni sono arrivate due notizie clamorose dal mondo dell’intelligenza artificiale applicata alla matematica: la formalizzazione completa della dimostrazione dell’“ultimo teorema di Fermat” e la soluzione (attualmente ancora da verificare) di un “problema del millennio” relativo alle equazioni di Navier–Stokes. Molte le reazioni, dall’entusiasmo dei tecno-ottimisti, alla paura dei tecno-pessimisti, fino alla preoccupazione di chi sostiene che l'interesse delle compagnie di IA alla soluzione dei grandi problemi aperti eroda gli aspetti culturalmente più rilevanti della ricerca matematica. Sono tutte reazioni comprensibili, e a parere dell'autore alcune sono anche molto ben motivate. Eppure, che le macchine contribuiscano in modo decisivo a dimostrare teoremi non dovrebbe sorprendere più di tanto. Per oltre un secolo, una piccola ma molto motivata comunità di matematici, e poi di logici e infine di informatici teorici, ha coltivato proprio questo sogno, oggi diventato realtà grazie al progresso tecnologico e a investimenti senza precedenti. (Illustrazione realizzata con strumenti di intelligenza artificiale generativa).