Abstract
This letter explores the philosophical consequences of AI-assisted theorem proving through a fictional letter set in the near future. It imagines a world in which an artificial proving system establishes the Birch and Swinnerton-Dyer conjecture with a formally verified proof that no human mathematician can fully understand. The essay argues that this possibility challenges the traditional unity of mathematical truth and understanding, suggesting that machine-generated mathematics may constitute a distinct form of mathematical practice. Rather than taking a stance for or against AI, it examines how formal verification, proof, and mathematical understanding may be reconfigured in an era of increasingly autonomous reasoning systems.
Questa lettera esplora le conseguenze filosofiche della dimostrazione automatica assistita dall’intelligenza artificiale attraverso una lettera immaginaria ambientata in un futuro prossimo. Il testo immagina un mondo in cui un sistema artificiale dimostra la congettura di Birch e Swinnerton-Dyer mediante una prova formalmente verificata ma incomprensibile ai matematici. Si sostiene che questa possibilità metta in discussione l’unità tradizionale tra verità e comprensione matematica, suggerendo che la matematica prodotta dalle macchine possa costituire una forma distinta di pratica matematica. Piuttosto che assumere una posizione favorevole o contraria all’IA, il saggio riflette su come verifica formale, dimostrazione e comprensione matematica possano essere ridefinite nell’era dei sistemi di ragionamento autonomo.
Citazione
Simone Severini, “Letter to Rozumot: Two (or More) Mathematicses”, in “APhEx 33”, 2026, pp. 302-322.
Numero della rivista
N°33/2026-APhEx
Visualizza e scarica il file PDF
Vai agli indici
AUTORI&AUTRICI
Distinguished Engineer presso Google e Professore di Fisica dell'Informazione presso l'University College London. Ricopre inoltre, tra gli altri incarichi, il ruolo di membro dello Strategic Advisory Board della Lean FRO. In precedenza, in qualità di General Manager per le Tecnologie Quantistiche presso Amazon Web Services, ha avviato e diretto i programmi di Amazon dedicati al calcolo quantistico, sviluppando collaborazioni con istituzioni come il California Institute of Technology (Caltech) e l'Università di Harvard. Ha inoltre contribuito alla fondazione di diverse aziende pionieristiche nel settore dell'hardware e del software quantistico, tra cui Cambridge Quantum Computing (oggi Quantinuum) e Phasecraft.
