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
"kaspar":perché no? Tutto serve... E soprattutto sapere un po' di teoria dei tipi rende attenti ai dettagli. Certe persone fanno matematica con la cazzuola.
Non è male dai...
Ecco sì, Agda non è sempre bello da leggere, visivamente. (Anzi, è molto brutto.) Su Lean si sta facendo molto lavoro per semplificare la vita all'utente --- o per nascondere molto lavoro sporco sotto il tappeto. D'altra parte non si può pretendere che un matematico conosca qualche TT. Oppure sì?
Non è male dai...
Ecco sì, Agda non è sempre bello da leggere, visivamente. (Anzi, è molto brutto.) Su Lean si sta facendo molto lavoro per semplificare la vita all'utente --- o per nascondere molto lavoro sporco sotto il tappeto. D'altra parte non si può pretendere che un matematico conosca qualche TT. Oppure sì?
Ecco sì, Agda non è sempre bello da leggere, visivamente. (Anzi, è molto brutto.) Su Lean si sta facendo molto lavoro per semplificare la vita all'utente --- o per nascondere molto lavoro sporco sotto il tappeto. D'altra parte non si può pretendere che un matematico conosca qualche TT. Oppure sì?
Quelle che intendevo è questo: un branch di agda, [inline]cubical-agda[/inline] è una implementazione di HoTT, cioè di una certa interpretazione di MLTT. E' un adagio comune che "non si fa matematica in MLTT", perché è una fondazione un po' troppo rigida per fare le cose veramente. Questa, ad esempio, è una dimostrazione in standard-agda che 2+2=4:
(source: PLFA, https://plfa.github.io/Lambda/ )
Quella che ho postato oggi invece era una dimostrazione di analisi fatta in Lean, essenzialmente in linguaggio naturale. Puoi apprezzare la rigidità del primo linguaggio, e la flessibilità del secondo.
_ : plus · two · two —↠ `suc `suc `suc `suc `zero
_ =
begin
plus · two · two
—→⟨ ξ-·₁ (ξ-·₁ β-μ) ⟩
(ƛ "m" ⇒ ƛ "n" ⇒
case ` "m" [zero⇒ ` "n" |suc "m" ⇒ `suc (plus · ` "m" · ` "n") ])
· two · two
—→⟨ ξ-·₁ (β-ƛ (V-suc (V-suc V-zero))) ⟩
(ƛ "n" ⇒
case two [zero⇒ ` "n" |suc "m" ⇒ `suc (plus · ` "m" · ` "n") ])
· two
—→⟨ β-ƛ (V-suc (V-suc V-zero)) ⟩
case two [zero⇒ two |suc "m" ⇒ `suc (plus · ` "m" · two) ]
—→⟨ β-suc (V-suc V-zero) ⟩
`suc (plus · `suc `zero · two)
—→⟨ ξ-suc (ξ-·₁ (ξ-·₁ β-μ)) ⟩
`suc ((ƛ "m" ⇒ ƛ "n" ⇒
case ` "m" [zero⇒ ` "n" |suc "m" ⇒ `suc (plus · ` "m" · ` "n") ])
· `suc `zero · two)
—→⟨ ξ-suc (ξ-·₁ (β-ƛ (V-suc V-zero))) ⟩
`suc ((ƛ "n" ⇒
case `suc `zero [zero⇒ ` "n" |suc "m" ⇒ `suc (plus · ` "m" · ` "n") ])
· two)
—→⟨ ξ-suc (β-ƛ (V-suc (V-suc V-zero))) ⟩
`suc (case `suc `zero [zero⇒ two |suc "m" ⇒ `suc (plus · ` "m" · two) ])
—→⟨ ξ-suc (β-suc V-zero) ⟩
`suc `suc (plus · `zero · two)
—→⟨ ξ-suc (ξ-suc (ξ-·₁ (ξ-·₁ β-μ))) ⟩
`suc `suc ((ƛ "m" ⇒ ƛ "n" ⇒
case ` "m" [zero⇒ ` "n" |suc "m" ⇒ `suc (plus · ` "m" · ` "n") ])
· `zero · two)
—→⟨ ξ-suc (ξ-suc (ξ-·₁ (β-ƛ V-zero))) ⟩
`suc `suc ((ƛ "n" ⇒
case `zero [zero⇒ ` "n" |suc "m" ⇒ `suc (plus · ` "m" · ` "n") ])
· two)
—→⟨ ξ-suc (ξ-suc (β-ƛ (V-suc (V-suc V-zero)))) ⟩
`suc `suc (case `zero [zero⇒ two |suc "m" ⇒ `suc (plus · ` "m" · two) ])
—→⟨ ξ-suc (ξ-suc β-zero) ⟩
`suc (`suc (`suc (`suc `zero)))
∎(source: PLFA, https://plfa.github.io/Lambda/ )
Quella che ho postato oggi invece era una dimostrazione di analisi fatta in Lean, essenzialmente in linguaggio naturale. Puoi apprezzare la rigidità del primo linguaggio, e la flessibilità del secondo.
L'hai detto tu.
HoTT non è un modo per fare matematica "vera";
Mi rendo conto che un messagio scritto può essere recepito diversamente da quello pensato.
È ovvio, poi, che non so cosa sia la "matematica vera".
Anche se non è matematica vera.Waitwhat
"marco2132k":
può essere utile leggersi l'HoTT book [...]?
Dipende da che "utilità". È una buona lettura, e alcune cose della parte "Mathematics" possono solo farti bene. Anche se non è matematica vera.
Puoi sempre provare, alla peggio lo molli se non ti interessa: succede niente.
Questo è quello che intendevo quando dicevo "col tempo sarà impossibile distinguere il linguaggio naturale dal codice di una dimostrazione assistita": https://github.com/PatrickMassot/lean-v ... ample.lean
Questo testo è codice valido che compila:
Più che sottolineare che questa è la stessa matematica che scriviamo in TeX, ma è già proofreadata da una macchina, non saprei cosa dire.
Questo testo è codice valido che compila:
/-
If f is continuous at x₀ and the sequence u tends to x₀ then the sequence f ∘ u, sending n to
f (u n) tends to f x₀
-/
example (f : ℝ → ℝ) (u : ℕ → ℝ) (x₀ : ℝ)
(hu : sequence_tendsto u x₀) (hf : continuous_function_at f x₀) :
sequence_tendsto (f ∘ u) (f x₀) :=
begin
Let's prove that ∀ ε > 0, ∃ N, ∀ n ≥ N, |f (u n) - f x₀| ≤ ε,
Fix ε > 0,
By hf applied to ε using ε_pos we obtain δ such that
(δ_pos : δ > 0) (Hf : ∀ (x : ℝ), |x - x₀| ≤ δ → |f x - f x₀| ≤ ε),
By hu applied to δ using δ_pos we obtain N such that Hu : ∀ n ≥ N, |u n - x₀| ≤ δ,
Let's prove that N works : ∀ n ≥ N, |f (u n) - f x₀| ≤ ε,
Fix n ≥ N,
By Hf applied to u n it suffices to prove |u n - x₀| ≤ δ,
This is Hu applied to n using n_ge,
endPiù che sottolineare che questa è la stessa matematica che scriviamo in TeX, ma è già proofreadata da una macchina, non saprei cosa dire.
@ 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.
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.
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.
"marco2132k":
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.
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.
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
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?
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?
"megas_archon":Aha noo quello è un corso di magistrale non me lo fanno fare.
Se la domanda è: vale la pena seguire il corso di teoria dei tipi di Milly? La risposta è sì.
"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?
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ì.
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?
Per dire, secondo voi questo approccio a (una parte di?) matematica diventerà comune più o meno come è diventato comune smanettare in Python + numpy?
che persino la teoria dei tipi (nata per scongiurare ogni paradosso) era affetta dal medesimo maleEh, ogni; magari.
"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?
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.
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.
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.
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.
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:
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.
- 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.
Accedi a tutti gli appunti
Tutor AI: studia meglio e in meno tempo