Le medaglie Fields avvertono: la matematica e le aziende di AI hanno obiettivi diversi

La tensione tra la comunità matematica e le aziende che sviluppano intelligenza artificiale non è più una discussione da corridoio. Su «Le Monde» è apparso un testo firmato da venticinque vincitori della medaglia Fields, il più alto riconoscimento in matematica. Gli autori scrivono che gli obiettivi delle aziende di AI e quelli della comunità matematica si allontanano profondamente. L'accusa non riguarda il fatto che i modelli risolvano problemi. Riguarda per quale scopo li si risolve e come lo si racconta.

Una dimostrazione non è un prodotto

Pochi giorni dopo, «Le Monde» ha pubblicato una conversazione con Stéphane Mallat, matematico all'ENS, insignito nel 2025 della medaglia d'oro del CNRS e coautore dell'algoritmo di compressione JPEG 2000. La sua frase è il filo conduttore di tutto il dibattito: le dimostrazioni eseguite dall'AI hanno poco valore in sé se non abbiamo una preparazione sufficiente a capirle. Mallat si occupa tra l'altro della maledizione della dimensionalità, il problema in cui il numero di configurazioni possibili cresce così rapidamente che non ha più senso cercare di farsi un'intuizione partendo dalle dimensioni basse.

L'argomento si può dire in modo concreto. La matematica non è solo un insieme di teoremi veri. È anche una tecnica per capire perché sono veri. Un verificatore confermerà la correttezza di una scrittura formale, ma non trasmetterà allo studente nessuna di queste capacità finché non sarà esposta e discussa.

Cosa sa fare oggi la verifica automatica

In parallelo nascono lavori che mostrano come si svolge una collaborazione seria tra uomo e macchina. In un articolo su arXiv, Mario Carneiro dimostra che nella teoria dei tipi dell'assistente Lean basta il principio del terzo escluso per dimostrare la coerenza della teoria degli insiemi ZF, e in forma completamente formalizzata. Niente assioma di scelta, niente estensionalità delle proposizioni, niente quozienti. È un risultato tecnico, ma ha un peso filosofico: finora si poteva pensare che senza l'operatore di scelta la forza della teoria dei tipi scendesse molto al di sotto di ZF.

Il secondo filone è la ricerca assistita dalla verifica. Il modello propone programmi in stile FunSearch, un valutatore rigoroso li giudica e la selezione lascia i migliori. Gli autori di uno di questi lavori hanno condotto l'esperimento persino su un laptop, con un modello locale da trenta miliardi e da 120 a 600 campioni verificati per esecuzione. Il risultato è ambiguo e proprio per questo prezioso. La ricerca si è fermata dopo aver colmato poco più del 90 per cento del divario dal record in un compito di punta. Quando al modello è stato dato un suggerimento sulla famiglia di costruzioni, il ciclo ha ottimizzato l'idea fornita, anche se nessuna delle esecuzioni autonome l'aveva scoperta.

Sullo sfondo resta la questione degli incentivi. Se il criterio più importante diventa il record in una tabella, la matematica si trasforma in un insieme di benchmark, non in una pratica di comprensione. La prudenza davanti a questa semplificazione non è ostilità verso gli strumenti: è la condizione perché gli strumenti siano davvero utili in modo duraturo.