Questione di Scholze & Clausen
Sentito della questione di Scholze & Clausen e del controllo delle loro dimostrazioni da parte di software?
Che ne pensi?
Che ne pensi?
Risposte
Veramente ti ho già risposto, ma...
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\)).
Per il resto, non c'è nessun bisogno che ripeta che cosa penso degli analisti numerici o di chi fa queste sciocche domande.
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).
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":
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.
- [*:sbcsrjb8]
"gugo82":
[quote="megas_archon"]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.[/quote]
[/*:m:sbcsrjb8]
[*:sbcsrjb8]
"gugo82":
[quote="megas_archon"]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é?[/quote]
[/*:m:sbcsrjb8]
[*:sbcsrjb8]
"gugo82":
[quote="megas_archon"]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 è?[/quote]
[/*:m:sbcsrjb8]
[*:sbcsrjb8]
"gugo82":[/*:m:sbcsrjb8][/list:u:sbcsrjb8]
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.
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.
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.
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.
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.
Quindi, una bella mazzata.
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.
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.
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?
"otta96":
Qual'era l'errore che hai citato?
Il link che ho postato ti porta direttamente all'errata. Ah dimenticavo che è un paper del 2004. Ci sono voluti 15 anni prima che qualcuno se ne accorgesse.
Qual'era l'errore che hai citato?
"Fioravante Patrone":
Un tool utile, ma a mio parere siamo molto lontani da una "rivoluzione culturale". Nella ricerca matematica quello che serve sono idee, intuizioni, visione, queste cose qui. Raramente le dimostrazioni sono importanti.
Questo poteva essere vero 100 anni fa, quando le dimostrazioni erano piuttosto semplici da controllare, ma certamente non lo è oggi, quando la ricerca teorica ha raggiunto orizzonti così avanzati che capire se una dimostrazione sia giusta o meno può essere un problema altamente non banale. E ci sono diversi esempi illustri, a partire dalla questione di Mochizuki (se non conosci la storia dai un'occhiata qua ed agli altri post sullo stesso blog), francamente uno dei punti più bassi raggiunti dalla comunità matematica negli ultimi anni. Questione che non sarebbe nemmeno esistita se la prova fosse tradotta in Lean. Inoltre la tua affermazione mi fa sospettare che tu non abbia letto e studiato approfonditamente molti paper di matematica teorica, perchè ti posso assicurare che il numero di errori nelle dimostrazioni è imbarazzante. Tanto per fare un esempio, uno dei paper più celebri degli ultimi 30 anni, PRIMES is in P, conteneva un errore. In questo caso è un piccolo errore che non inficia la correttezza del risultato, ma questo è uno dei paper più letti e studiati di sempre, ed è totalmente elementare! Immagina cosa succede in campi come il programma di Langlands, a cui lavorano pochissime persone al mondo che usano una montagna di strumenti iper tecnici la cui correttezza assume quella di una torre di risultati ognuno basato sul precedente.
E' chiaro che avere un sistema di controllo delle dimostrazioni probabilmente non ci porterà idee nuove su come attaccare l'ipotesi di Riemann (anche se non si può mai dire), ma certamente l'uso massivo di uno strumento così snellirebbe moltissimo il sistema e lo renderebbe verificato e verificabile al 100%. Scusa se è poco...
Un tool utile, ma a mio parere siamo molto lontani da una "rivoluzione culturale". Nella ricerca matematica quello che serve sono idee, intuizioni, visione, queste cose qui. Raramente le dimostrazioni sono importanti.
In effetti questa ha la potenzialità per essere una grossa rivoluzione culturale nella matematica. Probabilmente non succederà, ma vi immaginate un mondo in cui le prove dei teoremi, negli articoli scientifici, devono essere corredate da una loro versione in Lean? Questo snellirebbe enormemente il lavoro dei referee e soprattutto eliminerebbe l'insopportabile usanza di pubblicare dimostrazioni sbagliate. E a livello educativo, insegnare ad usare Lean agli studenti sarebbe il modo migliore di insegnargli cosa vuol dire dimostrare un teorema. Niente più domande del tipo "ma è giusta questa dimostrazione secondo voi?" Se è giusta per Lean, è giusta. Per chi fosse interessato, a questo link: https://www.ma.imperial.ac.uk/~buzzard/xena/natural_number_game/ si possono imparare in modo costruttivo le basi. Molto interessante, molto ben fatto.
Grazie per la dettagliata risposta 
Che poi Lean "dimostri da solo" i teoremi non è un'esagerazione: basta guardare qui https://www.youtube.com/watch?v=b59fpAJ8Mfs dove viene riprodotta a scopo didattico la dimostrazione di Euclide dell'infinità dei numeri primi (tra l'altro in una maniera costruttiva: per ogni $n\ge 1$, il minimo divisore primo di $n!+1$ è un primo maggiore di $n$).
Ovviamente, non c'è niente di veramente sorprendente nel fatto che una libreria di teoremi matematici riesca a "riempire i buchi" di una "semplice" dimostrazione di algebra elementare; se, però, iniziate a pensare che in questa libreria esiste la definizione di spazio di Banach...
Ovviamente, non c'è niente di veramente sorprendente nel fatto che una libreria di teoremi matematici riesca a "riempire i buchi" di una "semplice" dimostrazione di algebra elementare; se, però, iniziate a pensare che in questa libreria esiste la definizione di spazio di Banach...
Leggi qui https://en.wikipedia.org/wiki/Automated_theorem_proving ; 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".
Mi è stato chiesto cosa penso; penso che Lean (il theorem prover che lo Xena project ha utilizzato per certificare una parte del lavoro di Scholze-Clausen) sia estremamente espressivo e potente, perché un suo teorema certificato è praticamente indistinguibile da uno schema di dimostrazione che si usa per capire come è strutturato un argomento in matematica "discorsiva": per esempio, questo è codice Lean perfettamente funzionante,
Ovviamente questa dimostrazione è poco più di un esercizio per prendere mano con la sintassi di Lean (questo stile di dimostrazione usa dei costrutti detti "tattiche"; l'alternativa di altri dimostratori automatici è costruire dei "proof terms"). Quello che è soprendente è che queste definizioni presuppongono delle costruzioni altamente non banali; i numeri reali e le loro proprietà, le proprietà delle funzioni, etc. Implementare queste strutture in una macchina non è affatto banale; o meglio, quello che è ancor meno banale è essere riusciti a farlo in maniera che il linguaggio finale sia ragionevolmente leggibile da un matematico, e non solo da una macchina. Un'altra cosa impressionante è la quantità sconfinata di matematica che è già stata formalizzata: https://leanprover-community.github.io
Per esempio, questa è la definizione di spazio normato su un campo normato:
e questa è la definizione di spazio $L^p$:
Mi è stato chiesto cosa penso; penso che Lean (il theorem prover che lo Xena project ha utilizzato per certificare una parte del lavoro di Scholze-Clausen) sia estremamente espressivo e potente, perché un suo teorema certificato è praticamente indistinguibile da uno schema di dimostrazione che si usa per capire come è strutturato un argomento in matematica "discorsiva": per esempio, questo è codice Lean perfettamente funzionante,
example (h : surjective (g ∘ f)) : surjective g :=
-- ^ questo è l'enunciato del teorema, `surjective`
-- è definito precedentemente. Una dimostrazione è
-- tutto quello che è compreso tra `begin` ed `end`.
begin
unfold surjective at h,
-- ^ unfold serve a espandere la definizione di `surjective`,
-- che è questa:
-- ∀ (b : ℝ), ∃ (a : ℝ), (g ∘ f) a = b
-- (di nuovo questo codice è perfettamente legittimo:
-- è il modo in cui viene capito da Lean)
unfold surjective,
-- ^ stessa cosa, ma invece di espandere la definizione di
-- suriettività per h, lo si fa per g, che è la tesi che va dimostrata
intro b,
-- ^ si introduce la variabile b
specialize h b,
-- si specializza la definizione di suriettività,
-- che è un'asserzione quantificata universalmente,
-- per lo specifico elemento b
cases h with a ha,
-- ^ l'ipotesi `h` è una quantificazione esistenziale;
-- `cases` la spezza in una coppia < a , ha > dove `a` è
-- un elemento di ℝ, e `ha` una dimostrazione del fatto
-- che g ( f a ) = b
use f a,
-- `use` serve a iniziare la dimostrazione del fatto che
-- si può scegliere `f a` come testimone ("witness") del
-- fatto che g è suriettiva.
exact ha,
end e dimostra che se \(f , g : \mathbb R \to \mathbb R\) sono funzioni (reali di variabile reale, ma questa ipotesi non è fondamentale, basta editare un'altra parte del codice) con la proprietà che la composizione \(g\circ f\) è (definita e) suriettiva, allora anche $g$ è suriettiva. La dimostrazione va come viene spiegato nei commenti (le righe che iniziano con un [inline]--[/inline]).Ovviamente questa dimostrazione è poco più di un esercizio per prendere mano con la sintassi di Lean (questo stile di dimostrazione usa dei costrutti detti "tattiche"; l'alternativa di altri dimostratori automatici è costruire dei "proof terms"). Quello che è soprendente è che queste definizioni presuppongono delle costruzioni altamente non banali; i numeri reali e le loro proprietà, le proprietà delle funzioni, etc. Implementare queste strutture in una macchina non è affatto banale; o meglio, quello che è ancor meno banale è essere riusciti a farlo in maniera che il linguaggio finale sia ragionevolmente leggibile da un matematico, e non solo da una macchina. Un'altra cosa impressionante è la quantità sconfinata di matematica che è già stata formalizzata: https://leanprover-community.github.io
Per esempio, questa è la definizione di spazio normato su un campo normato:
@[class] structure normed_space (α : Type u_5) (β : Type u_6) [normed_field α] [normed_group β] : Type (max u_5 u_6) to_module : module α β norm_smul_le : ∀ (a : α) (b : β), ∥a • b∥ ≤ ∥a∥ * ∥b∥
e questa è la definizione di spazio $L^p$:
def Lp {α} (E : Type*) {m : measurable_space α} [measurable_space E] [normed_group E]
[borel_space E] [second_countable_topology E]
(p : ℝ≥0∞) (μ : measure α) : add_subgroup (α →ₘ[μ] E) :=
{ carrier := {f | snorm f p μ < ∞},
zero_mem' := by simp [snorm_congr_ae ae_eq_fun.coe_fn_zero, snorm_zero],
add_mem' := λ f g hf hg, by simp [snorm_congr_ae (ae_eq_fun.coe_fn_add _ _),
snorm_add_lt_top ⟨f.ae_measurable, hf⟩ ⟨g.ae_measurable, hg⟩],
neg_mem' := λ f hf,
by rwa [set.mem_set_of_eq, snorm_congr_ae (ae_eq_fun.coe_fn_neg _), snorm_neg] }
Cosa si intende per "riscrivere"? Lo chiedo con un background matematico scarso che ancora possiedo, non capisco bene cosa ci sia da riscrivere 
.
.
Un cofounder di Ethereum ha investito 20 milioni di dollari per fondare un "centro permanente col compito di riscrivere la matematica"
https://u.today/charles-hoskinson-donat ... -rewritten
https://twitter.com/IOHK_Charles/status ... 1183019017
https://u.today/charles-hoskinson-donat ... -rewritten
https://twitter.com/IOHK_Charles/status ... 1183019017
"megas_archon":
quando va bene, uno che fa analisi numerica sa l'algebra lineare, e nemmeno molto bene; quando va male, è per lo più quello che dovrebbe essere un ingegnere: una persona di pericolante istruzione matematica, che produce algoritmi di applicazione ingegneristica. Gli "ingegneri", invece, sono semplicemente [redacted]).
Eh niente, il "tiro all'ingegnere" rimarrà sempre in voga tra matematici e scienziati
"megas_archon":
quando va bene, uno che fa analisi numerica sa l'algebra lineare, e nemmeno molto bene; quando va male, è per lo più quello che dovrebbe essere un ingegnere: una persona di pericolante istruzione matematica, che produce algoritmi di applicazione ingegneristica. Gli "ingegneri", invece, sono semplicemente [redacted]).
Mi sento di dissentire su questo. Lasciami dire che questa idea dell' analisi numerica è significativamente distante dalla realtà.
Accedi a tutti gli appunti
Tutor AI: studia meglio e in meno tempo