Questione di Scholze & Clausen

[gugo82]

Sentito della questione di Scholze & Clausen e del controllo delle loro dimostrazioni da parte di software?
Che ne pensi?

[megas_archon]

P.S.: Sentito della questione di Scholze & Clausen e del controllo delle loro dimostrazioni da parte di software?
Che ne pensi?

Fino all'inizio del ventesimo secolo una caratteristica costituente del matematico era quella di saper svolgere conti molto complessi; determinanti di vandermonde generalizzati, integrali ellittici, alternanti doppi, circolanti, confluenti... per non parlare dei contazzi di geometria differenziale. Poi sono arrivati i computer: la schiena del matematico è stata alleggerita dall'onere di gestire la presenza di determinanti 9x9 (con il rischio di sbagliare e la certezza di annoiarsi). I CAS (Computer Algebra Systems) oggi non si contano nemmeno più.

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. Ovviamente è da qualche anno che sto imparando (anche) questa cosa; penso ne valga la pena e abbia un effetto importante sul grado di umiltà del matematico che si sottopone a questo cambio di prospettiva (uno dei primi esercizi che feci fu: dimostra che esiste una biiezione \(\mathbb N \cong \mathbb N\amalg \mathbb N\): da un lato c'è un'ovvia funzione iniettiva che manda i pari nella prima copia e i dispari nella seconda; dall'altro, l'idea ovvia è di definire \(k\mapsto 2k\) nella prima copia, e \(k\mapsto 2k+1\) nella seconda; c'è solo un problema, chi assicura al type checker che questa funzione sia iniettiva? Va dimostrato, per induzione -che è l'unico modo in cui le dimostrazioni che coinvolgono il tipo dei naturali possono farsi-. Insomma, ci si rende rapidamente conto di non aver mai fatto una dimostrazione prima di quel momento, ed è una bella scossa all'amor proprio).
Come tutti i cambiamenti questo genererà delle storture, per esempio quello che ha generato la nascita dell'analisi numerica (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]). Ci abitueremo, evolveremo, alcune cose resteranno le stesse, e altre cambieranno radicalmente.

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". 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 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.

[gugo82]

P.S.: Sentito della questione di Scholze & Clausen e del controllo delle loro dimostrazioni da parte di software?
Che ne pensi?

Fino all'inizio del ventesimo secolo una caratteristica costituente del matematico era quella di saper svolgere conti molto complessi; determinanti di vandermonde generalizzati, integrali ellittici, alternanti doppi, circolanti, confluenti... per non parlare dei contazzi di geometria differenziale. Poi sono arrivati i computer: la schiena del matematico è stata alleggerita dall'onere di gestire la presenza di determinanti 9x9 (con il rischio di sbagliare e la certezza di annoiarsi). I CAS (Computer Algebra Systems) oggi non si contano nemmeno più.

Sì, questo lo si sa. È storia.

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 quanto e come le dimostrazioni routinarie dovrebbero essere soppiantate da altro e da cos'altro.

Ovviamente è da qualche anno che sto imparando (anche) questa cosa

Sì, me lo ricordavo; per questo ti ho chiesto di commentare.

penso ne valga la pena e abbia un effetto importante sul grado di umiltà del matematico che si sottopone a questo cambio di prospettiva (uno dei primi esercizi che feci fu: dimostra che esiste una biiezione \(\mathbb N \cong \mathbb N\amalg \mathbb N\): da un lato c'è un'ovvia funzione iniettiva che manda i pari nella prima copia e i dispari nella seconda; dall'altro, l'idea ovvia è di definire \(k\mapsto 2k\) nella prima copia, e \(k\mapsto 2k+1\) nella seconda; c'è solo un problema, chi assicura al type checker che questa funzione sia iniettiva? Va dimostrato, per induzione -che è l'unico modo in cui le dimostrazioni che coinvolgono il tipo dei naturali possono farsi-. Insomma, ci si rende rapidamente conto di non aver mai fatto una dimostrazione prima di quel momento, ed è una bella scossa all'amor proprio).

Più che 'non aver mai fatto una dimostrazione', ti sarai reso conto che non hai mai fatto una dimostrazione nel senso in cui la intendono i Logici o i Filosofi della Matematica, ossia formalizzandone completamente tutti i passaggi.

Probabilmente, ancora, avrebbe potuto essere d'aiuto (contribuendo anche al 'grado di umiltà') sfruttare gli anni precedenti per confrontarsi con esseri umani -ancorché mascherati da uno schermo ed una tastiera-, piuttosto che ridursi a fare capire cose ad un compilatore.
Ma vabbè, arriverà anche quel tempo lì.

Come tutti i cambiamenti questo genererà delle storture, per esempio quello che ha generato la nascita dell'analisi numerica (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]).

Qui mi hai ricordato quel prof. che, durante una scuola estiva sulla teoria del potenziale non lineare, affermò: "Tutti gli altri metodi, tipo (segue elenco di tre/quattro metodi utilizzati per dimostrare esistenza di soluzioni di PDE nonlineari), sono tutti equivalenti, ed ugualmente inutili".
Al che, l'organizzatore, nonché ideatore di uno di quei metodi, si alzò e gli ricordò che senza risultati iniziali/parziali non si sarebbe potuto arrivare ad un risultato generale.
L'incremento del 'grado di umiltà' passa anche dal riconoscere i piccoli contributi degli altri.

Ci abitueremo, evolveremo, alcune cose resteranno le stesse, e altre cambieranno radicalmente.

Infatti, solo che vorrei riuscire a capire dove andremo, per cercare di indirizzare qualcuno. Al momento la mia preoccupazione è questa qui.

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.

Questo sembra quello che EELST descrivevano come la mia spiccata sensibilità si contrappone al tuo gretto materialismo maschilista in 'Cara ti amo', non trovi?
Oddio, materialismo no; piuttosto utilitarismo, ma siamo lì.

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 è?
Credo che bisognerebbe riflettere di più su queste cose.

---

Note

1. Cosa diversa da quanto accaduto col Teorema dei Quattro Colori, in cui la macchina si occupava dei calcoli necessari alla dimostrazione, non del controllo della stessa. ↑

[megas_archon]

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

Il punto è sempre il solito, che tu non hai idea di nient'altro che della poca matematica che hai fatto...

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 è?

Sì, c'è un problema molto profondo, enucleato per primo da Voevodsky, altra medaglia Fields; in un suo famoso scritto ha gettato le basi di quella che si chiama teoria dei tipi omotopica, una fondazione alternativa della matematica in cui è possibile far capire a un proof assistant cosa sono le classi di equivalenza modulo una relazione; la storia completa è che un suo paper conteneva un errore... ed è raccontata qui https://www.ias.edu/ideas/2014/voevodsky-origins

[gugo82]

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

Il punto è sempre il solito, che tu non hai idea di nient'altro che della poca matematica che hai fatto...

Proprio non lo capisci, eh... Eppure mi sembrava di essere stato abbastanza chiaro:

L'incremento del 'grado di umiltà' passa anche dal riconoscere i piccoli contributi degli altri.

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 è?

Sì, c'è un problema molto profondo, enucleato per primo da Voevodsky, altra medaglia Fields; in un suo famoso scritto ha gettato le basi di quella che si chiama teoria dei tipi omotopica, una fondazione alternativa della matematica in cui è possibile far capire a un proof assistant cosa sono le classi di equivalenza modulo una relazione; la storia completa è che un suo paper conteneva un errore... ed è raccontata qui https://www.ias.edu/ideas/2014/voevodsky-origins

Grazie per il riferimento.

Quanto al resto, buona ricerca.

***

EDIT: Ho leggiucchiato l'articolo, che diventa comprensibile per un non addetto ai lavori solo dalla metà in poi.
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 anni¹), 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...² Insomma, qual è (se c'è) il vero problema?

Inoltre, effettivamente, questa parte qui:

Sarebbe interessante definire routine, a questo punto, e se [aggiunta postuma di gugo82 ] e quanto e come le dimostrazioni routinarie dovrebbero essere soppiantate da altro e da cos'altro.

che hai dribblato in simpatia ( ), sarebbe interessante da discutere.

---

Note

1. Cosa che credo sia di una normalità assoluta nella storia della Matematica, e non vedo perché dovrebbe preoccupare: col tempo si aggiusta tutto, anche senza correre (verso dove?). ↑
2. Esempio classico: per Cauchy ogni serie di funzioni continue convergente intorno ad un punto aveva somma continua. ↑

[megas_archon]

Gli spazi di Bach, le sementi di Mozart...

[megas_archon]

Chi vuole, venga

Abstract

Lawrence Paulson: Formalising Contemporary Mathematics in Simple Type Theory

A long-standing question in mathematics is the relevance of formalisation to practice. Rising awareness of fallibility among mathematicians suggests formalisation as a remedy. But are today's proof assistants up to the task? And what is the right formalism?

A wide variety of mathematical topics have been formalised in simple type theory using Isabelle/HOL. The partition calculus was introduced by Erdös and R. Rado in 1956 as the study of “analogues and extensions of Ramsey’s theorem”. Highly technical results were obtained by Erdös-Milner, Specker and Larson (among many others) for the case of ordinal partition relations, which is concerned with countable ordinals and order types. Much of this material was formalised last year (with the assistance of Džamonja and Koutsoukou-Argyraki).

Grothendieck's Schemes have also been formalised in Isabelle/HOL. This achievement is notable because some prominent figures had conjectured that schemes were beyond the reach of simple type theory.

Some highlights of this work will be presented along with general observations about role of type theory in the formalisation of mathematics.



Zoom details

Topic: Lawrence Paulson (Topos Institute Colloquium)

Time: Jul 1, 2021 05:00 PM Universal Time UTC

Join Zoom Meeting

https://topos-institute.zoom.us/j/53448 ... NkM3Ewdz09

Meeting ID: 534 486 2882

Passcode: 65537

[feddy]

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à.

[Brancaleone]

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]

Related https://www.youtube.com/watch?v=alByz_LoANE