Questione di Scholze & Clausen

[Bokonon]

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?

Se la mia memoria non mi inganna, Goedel ha utilizzato proprio la formalizzazione di Whitehead e Russel per formulare il suo teorema...facendo appunto notare che persino la teoria dei tipi (nata per scongiurare ogni paradosso) era affetta dal medesimo male.

P.S. Non ricordo se l'ho letto nel famoso libro di Hofstadter o nel bellissimo libro di Penrose "La mente nuova dell'imperatore". Dico "bellissimo" perchè, a livello divulgativo, fornisce una descrizione analitica assai precisa di diversi teoremi matematici...tanto che il passo successivo (ovvero leggerne le dimostrazioni) diventa quasi semplice. Per il resto, saltate l'ultimo capitolo di entrambi i libri.

[megas_archon]

che persino la teoria dei tipi (nata per scongiurare ogni paradosso) era affetta dal medesimo male

Eh, ogni; magari.

[marco2132k]

Domanda: per lo studente medio (per ora diciamo di matematica, ma in realtà vorrei chiederlo anche per chi fa STEM in generale), può essere utile leggersi l'HoTT book e imparare agda/Lean/boh?

Per dire, secondo voi questo approccio a (una parte di?) matematica diventerà comune più o meno come è diventato comune smanettare in Python + numpy?

[megas_archon]

Domanda: per lo studente medio (per ora diciamo di matematica, ma in realtà vorrei chiederlo anche per chi fa STEM in generale), può essere utile leggersi l'HoTT book e imparare agda/Lean/boh?

Per dire, secondo voi questo approccio a (una parte di?) matematica diventerà comune più o meno come è diventato comune smanettare in Python + numpy?

Brevemente: no e no, per motivi diversi nel primo e nel secondo caso;
HoTT non è un modo per fare matematica "vera"; meglio di agda è lean; questo approccio diventerà più comune, ma probabilmente non tanto quanto numpy etc (perché l'aperto denso della matematica non è la teoria dei tipi o la formalization, ma cose brutte tipo equazioni differenziali, geometria algebrica, teoria dei numeri...).
Agda aiuta? Non molto. Lean aiuta? Credo di sì, è certamente più espressivo, e la maniera con cui fai le dimostrazioni è molto intuitiva, ma non è intuitivo il modo in cui scrivi il boilerplate che ti permette di fare dimostrazioni di una riga.

Vale la pena cercare di capirci qualcosa, allo stesso modo in (e per lo stesso motivo per) cui vale la pena sapere un po' di geometria differenziale anche se si fa tutt'altro nella vita, perché costringe a pensare in maniera diversa.

Se la domanda è: vale la pena seguire il corso di teoria dei tipi di Milly? La risposta è sì.

[marco2132k]

In breve: il motivo non può essere che i proof assistant che ci sono ora sono troppo difficili da usare?

Insomma, mi hanno detto che la routine di LAPACK per moltiplicare due matrici prende 13 parametri (o qualcosa di simile), eppure ora in triennale trovi corsi di "laboratorio computazionale" dove

Studio, tramite sviluppo ed uso di programmi, di svariati argomenti di matematica, fra i quali: Distribuzione dei numeri primi. Metodi crittografici (sostituzione, Hill, RSA). Autosimilarita` ed insiemi frattali (insiemi di Cantor, curva di Koch etc). Misura di Hausdorff, lemma delle contrazioni e Iterated Function Systems. Insiemi di Julia e di Mandelbrot. Paesaggi frattali, dimensioni frattale e del Box Counting. Tassellazioni del piano. Integrazione numerica di equazioni differenziali ordinarie e semplici problemi di Sistemi Dinamici. Primo sguardo ai fenomeni caotici nei sistemi dinamici.

Cioè, magari non diventerà comune che uno studente si metta a checkare le dimostrazioni del corso di metodi, ma un "laboratorio" dove si dimostrano al pc -ad esempio- cose di teoria dei gruppi (o, in generale, un corso il cui scopo sia espressamente quello di usare un proof assitant, non di capire come funziona) forse qualcuno prima o poi lo terrà, no?

Se la domanda è: vale la pena seguire il corso di teoria dei tipi di Milly? La risposta è sì.

Aha noo quello è un corso di magistrale non me lo fanno fare.

[megas_archon]

il motivo non può essere che i proof assistant che ci sono ora sono troppo difficili da usare?

Non sono esattamente amichevoli per il matematico quadratico medio, nel senso che devi saper usare un editor serio, per contribuire a un progetto devi saper usare git, etc etc. Ma no, non sono "difficili" da usare; imparare C è ESTREMAMENTE più difficile perché devi badare a sozzure da ingegnere di cui a un matematico importa meno dell'Eurovision.

Il fatto è che i matematici solitamente sono tecnofobi che diventano scimmie con la rabbia quando gli fai notare che "mandarsi avanti e indietro la bozza di un paper via email" non è esattamente il concetto di "controllo di versione" più intelligente che esista.
Del resto chi non ha queste competenze minime (git e un editor modale) nel 2021 e vuole fare matematica, a mio modo di vedere merita una fortissima schicchera sulle orecchie.

Per il resto, il corso di Milly fa esattamente quel che dici, non con la teoria dei gruppi, ma con dei fatti di base di teoria dei tipi (per esempio, ti fa vedere come dimostrare alcune cose costruttivamente, senza LEM, e dov'è il trucco che devi usare per rendere costruttiva una dimostrazione che non lo è... lo teneva insieme a Milly un caro collega: https://github.com/iblech?tab=repositor ... agda&sort=

Io contribuisco ormai abbastanza regolarmente ad agda-categories, la lib per teoria delle categorie in agda. E qualche tempo fa volevo mettermi a fare per esercizio qualche definizione di algebra lineare (diciamo, fino ai determinanti; sarebbe bello dimostrare Hamilton-Cayley...). Intendiamoci, è una cosa che hanno fatto in molti, ma è un esercizio istruttivo (una volta qualcuno mi disse che per imparare veramente a usare un linguaggio devi implementare in esso l'anello dei polinomi a coefficienti interi).

Queste ultime cose sono indubbiamente al livello di uno studente triennale, e certamente insegnano molte cose su agda/quel che è.
Qui dove sono, poi, il corso di programmazione funzionale insegna mediante un altro linguaggio a tipi dipendenti, Idris che non serve assolutamente a nulla nella vita vera ma insegna un sacco di paradigmi simpatici e piuttosto generali. Vedi anche https://www.youtube.com/watch?v=4i7KrG1Afbk
Tutto ciò comunque è un po' OT, sorry.

Se vuoi vedere qualcosa di concreto, ci sentiamo e ti mostro in cosa consiste. Giuro di restare vestito.

[hydro]

Cioè, magari non diventerà comune che uno studente si metta a checkare le dimostrazioni del corso di metodi, ma un "laboratorio" dove si dimostrano al pc -ad esempio- cose di teoria dei gruppi (o, in generale, un corso il cui scopo sia espressamente quello di usare un proof assitant, non di capire come funziona) forse qualcuno prima o poi lo terrà, no?

E' possibile, ma secondo me inutile. Per come la vedo io al momento i proof assistant possono essere utili a due categorie di persone: in primis i matematici professionisti, per tutti i motivi di cui si diceva sopra, e in secondo luogo chi si approccia alla matematica. Spesso infatti il grande scoglio da superare per gli studenti del primo anno è capire cosa vuol dire dimostrare un'affermazione. Questo si ritrova in tante delle domande che vengono postate su questo forum, del tipo gente che scrive una serie infinita di simboli e quantificatori per provare che se $f: A\to B$ è una mappa iniettiva di insiemi finiti allora $|A|\leq |B|$ e poi chiede se la dimostrazione è giusta. Usare un proof assistant non solo renderebbe possibile rispondersi da soli, ma addirittura potrebbe avere il pregio di farti capire in che modo vanno concatenati gli step logici. D'altra parte per chi ha superato questo scoglio scrivere dimostrazioni di fatti di un corso di teoria dei gruppi della triennale in Lean penso sia più che altro uno spreco di tempo, perchè quelle sì possono facilmente essere controllate da mente umana.

[megas_archon]

Ma il punto non è necessariamente controllare la dimostrazione del teorema di Lagrange; il punto è scrivere una base di codice con cui verificare argomenti più complessi che lo usano. La cattedrale si fa dalle fondamenta, e le fondamenta sono noiose da gettare, ma serve perizia.

[gugo82]

@ megas_archon: Grazie per le risposte, come al solito dettagliate e dotte.
Per motivi personali non riesco a concentrarmi sufficientemente per scrivere nel dettaglio ciò che sento riguardo alle motivazioni che hai illustrato. Appena potrò cercherò di esporre qualche considerazione in merito.
Buone feste e grazie di nuovo.

[megas_archon]

https://arxiv.org/pdf/2112.11598.pdf intanto che ti riprendi, questo è rilevante.