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.
<br/>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.
