Ecco una domanda importante con cui dobbiamo confrontarci sempre di più man mano che i pipeline AI-per-Matematica diventano più comuni: Perché ci interessa risolvere problemi difficili? Quasi sempre, la risposta *non* è perché vogliamo particolarmente che il problema difficile venga risolto. (1/12)

Domande come l'esistenza di soluzioni globalmente lisce per le equazioni di Navier-Stokes sono di interesse matematico non perché la risposta stessa sia terribilmente importante, ma perché abbiamo motivo di credere che il processo di *scoprire* la risposta sia molto probabile... (2/12)

...per fornire nuove e profonde intuizioni nell'analisi, nelle PDE, nella dinamica dei fluidi, ecc., con nuove tecniche da sfruttare. Risolvere Fermat ci ha dato (indirettamente) il programma di Langlands. Risolvere Poincaré ci ha dato il flusso di Ricci. Si spera che risolvere Navier-Stokes ci dia qualcosa di altrettanto monumentale. (3/12)

Infatti, identifichiamo tali problemi come "interessantemente difficili" proprio perché intuendo che rappresentano un "gap" nella nostra attuale comprensione e nei nostri metodi. È per questo che i ciarlatani che affermano di risolvere (diciamo) l'ipotesi di Riemann usando "trucchi" o metodi elementari... (4/12)

...stanno in qualche modo perdendo di vista il punto: se uno di questi grandi problemi si rivelasse risolvibile utilizzando solo le attuali intuizioni matematiche e la tecnologia, sarebbe una delusione immensa: una sorgente che pensavamo stesse zampillando è, in realtà, asciutta. (5/12)

Cosa c'entra questo con l'AI? Beh, se si accetta il presupposto che i problemi difficili siano per lo più interessanti a causa delle nuove intuizioni e comprensioni che forniscono, sorge la domanda (alla luce degli sviluppi dell'AI): chi è responsabile della parte "comprensione"? (6/12)

Prendi le dimostrazioni per esaurimento (come nel teorema dei quattro colori), che sono state a lungo considerate piuttosto controverse, perché forniscono la parte di "certezza epistemica" di una dimostrazione, senza necessariamente fornire alcuna della parte di "intuizione" (che è di solito ciò che ci interessa) (7/12)

Pertanto, le dimostrazioni per esaurimento non sono certamente "sbagliate", ma in un certo senso sono "imbrogliate", o forse "autodistruttive": chiudono un problema potenzialmente fruttuoso, mentre eludono precisamente quegli aspetti della matematica che la rendono interessante e degna di essere affrontata. (8/12)

Penso che le prove generate da AI, in assenza di qualsiasi livello di comprensione o intuizione da parte dell'essere umano che le ha generate, dovrebbero essere considerate in modo molto simile. Se generi automaticamente una prova Lean di un grande teorema, è fantastico! Ma perché lo hai fatto? (9/12)

Se non comprendi i nuovi approfondimenti/metodi contenuti nella prova, allora tutto ciò che hai fatto è spostare il peso intellettuale da te stesso a chiunque sia disposto a leggerlo e comprenderlo (e, si spera, a comunicare gli approfondimenti ivi contenuti ad altri). (10/12)

La matematica è in ultima analisi un artefatto culturale umano (probabilmente il nostro più profondo, ricco e antico). Risolvere problemi difficili doveva essere solo un *proxy* per estendere quell'artefatto. L'AI sta rendendo emozionantemente facile generare nuovi percorsi di comprensione matematica.. (11/12)

...all'interno di quell'artefatto, ma sta anche rendendo più facile che mai raggiungere il proxy (cioè risolvere problemi difficili), mentre si perde di vista il motivo per cui ci interessava in primo luogo (cioè approfondire la nostra comprensione). Per favore, non farlo. (12/12)