Questione di Scholze & Clausen

[otta96]

Non me lo fa vedere, comunque a proposito di errori avevo sentito dire che Godel aveva trovato degli errori logici nei "Principi di geometria" di Hilbert e nei "Principia Mathematica" di Whitehead e Russel, qualcuno sa che errori sono o come dovrei fare per scoprire quali sono?

[gabriella127]

Ciao otta96.

Credo che, per quanto riguarda i Principia mathematica, trovi la critica di Gödel nel suo saggio Russel's mathematical logic.
Lo trovi in Benacerraf P., Putnam H. (eds.), Philosophy of Mathematics. Selected Readings.

Non so in rete.

[gabriella127]

Scrive Gödel in Russel's Mathematical Logic, a proposito dei Principia mathematica: "It is to be regretted that this first comprehensive and thorough going presentation of a mathematical logic and the derivation of Mathematics from it is so greatly lacking in formal precision in the foundations ( *1-*21 of Principia), that it presents in this respect a considerable step backwards as compared with Frege". etc.etc. (in Benacerraf etc.), p. 448.


Quindi, una bella mazzata.

[otta96]

Grazie Gabriella127 dei tuoi commenti, in effetti Godel ci va giù pensante, però almeno nel pezzo che hai riportato non dice esattamente cosa intende, cioè in cosa consisterebbe in pratica questa mancanza di precisione.

[gabriella127]

No, ma infatti, quello è all'inizio dell'articolo, l'ho scritto per dare una idea di come Gödel si pone criticamente rispetto ai Principia, poi c'è tutto l'articolo, non l'ho letto.
Continua dicendo che "what is missing, above all, is a precise statement of the syntax of the formalism". E poi va avanti per venti pagine a esaminare i Principia. . Quindi immagino che parlerà di qualche cosa che non gli quadra.
Caso mai lo leggerò, ora non so dirti di più, tranne che trovo probabile che in questo scritto ci siano quegli errori a cui ti riferivi.

[gugo82]

questo thread è nato perché mi hanno chiesto cosa penso della "intrusione" dei dimostratori automatici per certificare la correttezza della dimostrazione di Scholze-Clausen (vedi qui https://www.nature.com/articles/d41586-021-01627-2 e in particolare la quote di Scholze "[...] interactive proof assistants are now at the level that, within a very reasonable time span, they can formally verify difficult original research".

In realtà no, la domanda non era questa, o almeno non riguardava solo quest'aspetto della questione (come ho detto diverse volte)... Poi, vabbé, c'è stato un mio più o meno lungo iato dal forum e la discussione è finita a magnificare la potenza di LEAN.

I punti sensibili (perché "di senso") della questione credo siano altri, e ti riporgo le domande.

• Oggi sta succedendo una cosa simile, con la differenza che invece che liberare il matematico dall'onere di svolgere conti di routine, lo si sta liberando dall'onere di svolgere dimostrazioni di routine.

  
  Sarebbe interessante definire routine, a questo punto, e quando e quanto e come le dimostrazioni routinarie dovrebbero essere soppiantate da altro e da cos'altro.

  
  

• Se la domanda è "funziona?", la risposta è "indubbiamente sì, e dovresti imparare: basta un laptop e mezz'ora di tempo per installare l'ultima versione di agda".

  
  "Indubbiamente" perché?
  Secondo te chi programma questi sw ha maggiore perizia del generico Analista Numerico? E, se sì, perché?

  
  
  

• Se la domanda è "cosa pensi del fatto che Scholze e Clausen abbiano checkato la bontà di una dimostrazione attraverso un proof assistant", la mia risposta è che purtroppo le persone sono per la maggior [parte, aggiunta di gugo82 ] scimmie a cui serve una ragione per imparare le cose; non le imparano perché sono giuste o belle, ma solo nella misura in cui servono loro. Per queste ragioni, "fare pubblicità" a una "matematica augmentata", così chiamata perché giustappone un'intelligenza, il proof assistant, a un'altra, il matematico, è utile: perché convince i nabbi.

  
  [...] Il punto è che non credo, come pare nemmeno tu (libero di smentire questa mia illazione), alla storia di un giovane medagliato Fields che ha bisogno di farsi controllare una dimostrazione da una macchina.
  Il punto da chiarire è: perché si sente o perché dovrebbe sentirsi (in alcune branche della Matematica piuttosto che in altre) questa necessità?
  C'è un problema da qualche parte? Se sì, qual è?

  
  

• Capisco l'idea di fondo, ma non credo che quanto ho letto risponda alla domanda: infatti, non chiedevo il perché motivazionale (ci sono errori che si scoprono dopo quasi 20 anni1), ma la causa del non vedere questi errori che, a quanto capisco, non dipendono da mancanza nella conoscenza delle regole del gioco, delle strutture di base, etc...2 Insomma, qual è (se c'è) il vero problema?

Inoltre, mi pare che Scholze stesso abbia un buon motivo per spingere su questa faccenda del controllo automatico delle dimostrazioni, che risale a quando ha contribuito ad affossare alcuni articoli di Mochizuki.

[megas_archon]

Veramente ti ho già risposto, ma...

Sarebbe interessante definire routine, a questo punto, e quando e quanto e come le dimostrazioni routinarie dovrebbero essere soppiantate da altro e da cos'altro.

Una "dimostrazione di routine" è una che deve solo "fare un conto", applicare uno schema di dimostrazione generale in un caso particolare, o segue da una sequenza ordinata di manipolazioni sintattiche. Molte dimostrazioni sono tali, ma "sembra" che contengano un'idea per lo stesso motivo per cui "sembrava" che un procedimento per calcolare un risultante contenesse un'idea prima che il mero calcolo venisse automatizzato. Molte dimostrazioni in topologia generale, ad esempio, sono "di routine"; ma è complicato automatizzarle perché è complicato spiegare a una macchina cos'è uno spazio topologico (c'è un problema irrimediabile sotto). Lean, per esempio, ci riesce.

L'idea è semplice: interpretando la matematica in sistemi di tipi sempre più espressivi è possibile automatizzare dimostrazioni che avvengono sempre più ad alto livello. Interpretandola in un sistema di tipi con i giusti assiomi, è persino possibile maneggiare oggetti dal carattere prettamente infinitario (che ne so, ad esempio i Boreliani di \(\mathbb R\)).

Secondo te chi programma questi sw ha maggiore perizia del generico Analista Numerico? E, se sì, perché?

Ha una competenza ortogonale a quella di cui parlo, sebbene entrambe si sostanzino nel "programmare un algoritmo". Chi programma questi software solitamente è un bravo logico la cui competenza matematica spazia abbastanza in largo. Posso farti dei nomi.
Per il resto, non c'è nessun bisogno che ripeta che cosa penso degli analisti numerici o di chi fa queste sciocche domande.

l punto da chiarire è: perché si sente o perché dovrebbe sentirsi (in alcune branche della Matematica piuttosto che in altre) questa necessità?

La storia di Voevodsky lo spiega bene: alcune dimostrazioni si sono rivelate troppo convolute per poter essere verificate da un referee umano; nel lavoro di V. c'erano dei (relativamente gravi) errori, senza che ci si mettesse di mezzo la malizia di nessuno a non vederli, che hanno compromesso una parte della ricerca altrui.

Hai mai referato un paper? Sei familiare con il meccanismo di auctoritas che produce un bias in come le pubblicazioni vengono valutate? "Si assume" che Martin Hairer abbia più diritto di scrivere che "la dimostrazione del seguente fatto è omessa perché ovvia" di un gugo82 qualsiasi. Questa assunzione è formalmente errata, ma è diventata una prassi perché fa risparmiare tempo e alla fine i matematici bravi hanno ragione "anche quando hanno torto".

Fare altrimenti, cioè fare il pelo alla dimostrazione dei miei teoremi-farsa come lo si fece alla prova che Primes is in P, sarebbe un investimento di tempo enorme e poco motivato; tanto piu che i referee leggono gratis; regolamentare il loro mestiere sarebbe il primo passo verso una rimozione del bias di autorità di cui parlo, e del resto il punto è che la matematica formalizzata annulla il problema alla radice, perché in un ipotetico universo alternativo dove formalizzare le proprie dimostrazioni è la prassi, Hairer avrà buone idee usate perché giuste, in maniera perfettamente indipendente dalla sua autorità, e io e te avremo delle idee un po' meno buone, usate perché giuste, in maniera perfettamente indipendente dalla nostra assenza di autorità.

Ora, il fatto è che la gente pensa che usare questi proof assistant sia difficile e in ultima istanza allontani dalla prassi matematica. Primo: non è vero, il linguaggio in sé è solo leggermente più astratto di quelli commerciali. Secondo, è vero il contrario, come ho detto a me sembra di fare matematica molto meglio, da quando ho imparato qualcosa in questo senso.

Semplificando al limite del legale, questo genere di cose dovrebbe essere patrimonio del matematico medio perché formalizzare a questa maniera la matematica rende non impossibile, ma certamente molto meno semplice non notare errori simili, che sono legati al fatto che la matematica che si impara all'università è (per motivi storici e di convenienza espositiva) prettamente dialogica (la dimostrazione viene costruita come una serie di ordini impartiti verbalmente, in un linguaggio che sta a un linguaggio formalizzato / tipato nello stesso rapporto in cui il codice di un qualsiasi linguaggio di programmazione sta allo pseudo-codice).

Insomma, qual è (se c'è) il vero problema?

Credo di aver già risposto: la lunghezza e complessità quasi sovrumana di certe dimostrazioni; la natura dialettica di cui sopra che "intorta" autore e referee; la natura elusiva di certe strutture definibili ad un ordine maggiore del primo...

[megas_archon]

Per quanto riguarda Scholze, le cose sono andate circa così (ne ho sentito parlare Buzzard a quel famoso talk che linkavo): lui ha chiesto alla comunità dei proof-assistant se fosse possibile formalizzare una dimostrazione in un suo ultimo lavoro; questa comunità è fatta da tre tribù, una per ogni linguaggio di programmazione.

- Coq: non ha risposto
- Agda: non ha risposto
- Lean: Buzzard è riuscito a implementare qualcosa (insieme ad altri), ha scritto a Scholze e gli ha detto "al momento sappiamo fare questo". Scholze ha detto "molto bene; andate pure avanti se volete, ma avete già dimostrato il pezzo che mi interessava". Questo è stato l'endorsement di Scholze. Che, credo, poi, abbia iniziato a magnificare le potenzialità di Lean.

Per quanto riguarda te: non mi sembra di aver detto niente di strano, e ho ripetuto diverse volte questo concetto: certe dimostrazioni contenevano errori che, data la particolare struttura del ragionamento, erano difficili da scoprire. Voevodsky allora ha deciso di approcciare il problema alla radice, proponendo una fondazione della matematica alternativa per "risolvere il problema" (risolverlo compiutamente non si può; si può cercare di arginare certe cattive pratiche).

Il concetto di "cattiva pratica" lo devi intendere pressappoco come lo intendono i programmatori: il codice (la dimostrazione) gira (funziona/si capisce), ma "non si fa così", perché non risponde a certe caratteristiche base di ergonomia / modularità che rendono il codice (la dimostrazione) esportabile ad altri contesti.

Nel thread sul trinitarismo computazionale poi si diceva che esiste un motivo tecnico molto profondo per cui queste due cose sono esattamente la stessa

- la dimostrazione di un enunciato $P(x)$;
- del codice che, mangiando $x$, sputa $P(x)$.

Il fatto è che questo commento:

Il punto è che non credo, come pare nemmeno tu (libero di smentire questa mia illazione), alla storia di un giovane medagliato Fields che ha bisogno di farsi controllare una dimostrazione da una macchina.

sembra tradire la tua opinione sulla faccenda: che "farsi controllare una dimostrazione da una macchina" significhi aver sporcato la prassi dell'attività dimostrativa introducendo un elemento estraneo, che poco ha a che fare con ciò che la matematica è veramente. Questa è una postura da -diciamo- "boomer" della matematica: un individuo che l'ha appresa più di una generazione fa, e che non ha frequentazioni nel circolo di chi sta facendo matematica hic et nunc, 2021. "Farsi controllare una dimostrazione da una macchina" non va a detrimento della dimostrazione; è un modo come un altro per arrivare al QED; tra l'altro col vantaggio di evitare una intera classe di errori da cui la macchina è esente e a cui invece l'umano è abbastanza prono.

Spero che non ti offenda la banale verità per cui la matematica è progredita da quando ho finito il mio dottorato, figurati da quando hai finito il tuo; e se alcuni andazzi sono mode passeggere, c'è una dinamica dominante sottesa a dove la matematica di oggi sta andando, che probabilmente farà parlare degli anni '20 del XXI secolo alla stregua di come si parla oggi del lavoro di Hopf, Vietoris, Adams, Cech, Brouwer, Nevanlinna, Julia, Tonelli... (sto pescando dal parco piu ampio che conosco persone che sono stati capofila o esponenti illustri di una "scuola", un "movimento" o padri di una "teoria" di qualche tipo).

Sta andando a parare in quella che faccio io? No, o perlomeno: io faccio quello che faccio perché ritengo abbia un futuro; credere il viceversa (qualcosa ha un futuro in forza del fatto che è fatto da me) sarebbe abbastanza megalomane.

Semmai, quindi, io credo nella potenzialità di queste idee in forza di argomenti vissuti sul campo, in forza dell'essere stato nella stessa stanza (per fortuna, pre-Covid) con persone di visione piuttosto larga.

[hydro]

Condivido in toto quello che dice megas_archon, e in più vorrei sottolineare il fatto che si sta correndo (o forse ci siamo già pienamente dentro) un rischio anche peggiore: quello della stratificazione degli errori. Gli articoli pubblicati devono essere esenti da errori non solo perchè è giusto così, ma anche perchè i ricercatori che li leggono devono poter usare i risultati senza conoscere tutti i dettagli delle dimostrazioni. Cosa che ovviamente tutti già fanno, peccato che una dimostrazione che usa un risultato falso sia sbagliata. Quindi più si pubblicano cose sbagliate più ci sarà un'amplificazione del numero di errori in giro. Adesso siamo ancora ad un livello per cui i grandi esperti di un settore sono più o meno in grado, leggendo un paper, di capire se il risultato e la sua prova sono, nella loro essenza, giusti o sbagliati, ma tra 50 o 100 anni probabilmente non sarà più così, anche i maggiori esperti al mondo dovranno "fidarsi" della letteratura.

[megas_archon]

Sì, ci sono interi rami di ricerca che sono morti perché l'abstract del paper Y era "Questo è un controesempio al paper X", e l'abstract del paper Z era "questo invece è il motivo per cui sia X che Y contengono un errore". Dopo un paio d'anni di questo, non è cattiveria, ma la ricerca smette. E si fa altro, concentrandosi su aree dove si sa distinguere cosa è vero e cosa no.

La geometria algebrica italiana dell'inizio del '900 forse è un altro esempio, sebbene sia stata sistematizzata (per la maggior parte) da Grothendieck e non da un computer. Del resto proprio la gente che lavora in geometria enumerativa o teoria dei numeri algebrica, o geometria aritmetica, si fa spesso aiutare da magma e co., no?

In effetti, per diversi motivi questo accade in aree della matematica prettamente ad alta tecnologia (geometria e topologia algebrica erano le aree dove Voevodsky ha sollevato il problema; Mochizuki diceva di aver risolto un problema di teoria dei numeri -prima che proprio Scholze sottolineasse un gap piuttosto ampio nel suo argomento).

Disponendo di un metodo per verificare formalmente la correttezza delle dimostrazioni, entrambi gli imbarazzi sarebbero stati risolti.