Questione di Scholze & Clausen

[megas_archon]

"gugo82":Proprio non lo capisci, eh...

Ad illazione ho risposto con illazione; comunque hai ragione, mi dispiace, è stato un lapsus dato dal fatto che ti ho risposto molto tardi, piuttosto stanco, dopo essermi ripromesso di aspettare proprio per misurare le parole. Non avrei dovuto porla così, semplicemente l'idea che "pensi quel che pensi perché hai passato il tempo a istruire un computer invece di parlare con le persone" mi sembra sullo stesso piano di "pensi quel che pensi perché hai visto poche cose, e hai pochi riferimenti culturali/bibliografici". Che l'una illazione sia vera o falsa, lo prova il livello a cui interagiamo, la varietà delle topiche in cui dimostriamo di essere competenti, e il rigore e la generalità con cui rispondiamo o facciamo domande. Il mio e il tuo si confrontano da un po'; che conclusioni trae chi legge, in termini di competenza? (Di quella parlo, perché di quella qui si parla: le buone maniere non c'entrano nulla, né dovrebbero interferire con le competenze matematiche.)

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

Questa convinzione io la trovo ingenua, e frutto di una visione ingenua della matematica e della sua pratica: come se ci fosse un concetto di dimostrazione che è un processo culturale, e uno che è appannaggio dei logci e dei filosofi, e i due non fossero interdefinibili e dipendenti l'uno dall'altro. Come se la nozione di dimostrazione non fosse possibile formalizzarla compiutamente e trattarla come un oggetto matematico a sua volta. Ora, il fatto è questo, se mi fai delle domande ti rispondo, ma la tua volontà di essere convinto di qualcosa senza avere le competenze per apprezzare la risposta genera una discussione sterile (nella migliore delle ipotesi) o un litigio (nella peggiore).

Tralascio poi il fatto che hai deragliato la conversazione di proposito, invece di aprire un altro thread (come sarebbe stato tuo potere fare), se non altro perché questo genere di puntigli non mi interessano.

[j18eos]

[ot]

"gugo82":[...]Il problema è "il" in "il suo duale", soprattutto se vuoi considerare qualche spazio vettoriale 'decente' (con qualche struttura in più di quella puramente algebrica, e.g., quelli di Bach o quelli topologici) e non i polinomi.[...]

qVesto Zpiega mooolte coZe! [/ot]

[megas_archon]

E invece niente, ho trovato un controesempio prima di fare il conto.

[megas_archon]

Chiedevo [...] 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?

Cosa significa "dimostrare un teorema"? Una volta che hai risposto a questo in maniera soddisfacente hai capito qual è il problema, cioè che i due modi di intendere la parola, in senso sociale e in senso formale sono diversi, ma sono anche complementari, e interdefinenti l'un l'altro.
Questa è pure storia, risale a Hilbert, Gentzen ed altri che hanno definito quella che oggi si chiama "teoria della dimostrazione". In breve, la pratica matematica si consuma in questo dualismo inescapabile: da un lato, una dimostrazione come abbiamo imparato a farle da matricole è una lallazione appena più elaborata di quella di un bambino. Dall'altro, una dimostrazione completamente formale è incomprensibile a un umano, e -peggio- impossibile da comunicare a un altro umano.

Ora, il problema con Voevodsky è in realtà due problemi: da un lato, la struttura di alcune dimostrazioni è troppo complessa per poter essere controllata da mano umana -e quindi si fanno errori non perché non si ha una visione chiara delle strutture sottostanti, ma perché proprio la natura sociale, retorica del processo dimostrativo genera suggestioni[nota]il vocabolario informale è famoso per essere pieno di ambiguità, che solitamente sono innocue, e raramente invece fanno malissimo[/nota]. Suggestioni che, data la complessità[nota]nel senso Shannon del termine! Sono dimostrazioni estremamente strutturate, che si appoggiano a centinaia di preliminari, e che non sono ovvietà nemmeno quando le hai inquadrate nel giusto luogo e con il giusto linguaggio[/nota] dell'argomentazione sono difficili -se non impossibili- da controllare[nota]La natura sociale del discorso matematico si mostra nella sua maniera più peculiare quando un matematico B deve vidimare un risultato di un matematico A; ci fidiamo perché lo dice B, oppure ci fidiamo perché è "veramente vero"? Qui si esprime quella tensione di cui parlo: pendere troppo da ciascun lato fa sprofondare nel baratro, bisogna mantenere una via mediana. Una lettura tra tante: https://mathoverflow.net/questions/3784 ... athematics[/nota].

Il secondo problema è più profondo: "sì, ma quindi, come si fa?"
Nel senso che abbondano i sistemi di computer algebra, che svolgono integrali, trovano basi di Grobner, trovano polinomi minimi per calcolare gruppi di Galois... invece una maniera di "far fare i conti di topologia/geometria-topologia algebrica a una macchina" manca(va). Voevodsky ha proposto una fondazione alternativa della matematica dove questo è possibile.

Un esempio che a suo tempo fece abbastanza scalpore fu l'aver verificato formalmente la dimostrazione che il gruppo fondamentale del cerchio è Z. Ora, l'importanza di questo risultato non è nel teorema che dimostra, ovviamente, ma nell'aver provato che è possibile riuscire a formalizzare una dimostrazione che è ineliminabilmente "trascendentale all'algebra" (si fa uso di un po' di analisi, inescapabilmente, e in particolare del lemma dei numeri di Lebesgue e di alcuni fatti elementari sull'integrazione lungo cammini).

Negli anni a seguire sono stati dimostrati (o meglio "controllati") in questa maniera diversi altri teoremi di topologia algebrica. Un esempio importante è il teorema di Blakers-Massey, che è un risultato abbastanza profondo che esprime la connettività della fibra di una certa funzione continua ottenuta a partire da due funzioni date in termini delle connettività di queste ultime (un caso particolare di questo teorema: una mappa si dice "semplicemente connessa" se tutte le sue fibre sono semplicemente connesse; date due mappe semplicemente connesse, la fibra del loro prodotto fibrato ha una connettività più alta, il teorema dice quanto più alta). Anche qui, l'importanza del traguardo risiede nel fatto che per la prima volta è possibile formalizzare dimostrazioni che non coinvolgono numeri e operazioni tra numeri, ma insiemi (strutturati), operazioni tra insiemi strutturati, e invarianti -come ad esempio i gruppi di omologia e omotopia- ad essi associati.

Vuol dire molto di più, ma questo è un capitolo piuttosto lungo, che non ho le forze di comprimere in meno di un trattato. In breve, va così:

1. Se una categoria è abbastanza grande, essa si può pensare come un universo matematico, nel senso che la sua struttura interna permette di trattare i suoi oggetti come se fossero insiemi, i suoi morfismi come se fossero funzioni, ed è possibile ragionare al suo interno a proposito di tutte le costruzioni matematiche. Questa prospettiva è fruttuosa, perché permette di parlare -ad esempio- di strutture interne -i gruppi topologici- semplicemente come "quella cosa che è un gruppo, se il mio universo di riferimento è la categoria degli spazi topologici e non quella degli insiemi".

2. C'è però molto di più: se la categoria che eleggi a universo è abbastanza ricca, dentro di essa si può definire quello che si chiama un "linguaggio interno": è un linguaggio nel senso formale del termine, che se è abbastanza potente ti permette di fare tutto quello che facevi nella categoria degli insiemi (tutto significa "tutto": ci sono i numeri reali, gli spazi di funzioni, il calcolo delle variazioni, la geometria differenziale...).

3. Quindi, ogni categoria sufficientemente grande e ricca di struttura è un universo in grado di catturare una o più teorie matematiche; le categorie dove fai teoria degli insiemi si chiamano topos (di Grothendieck o elementari), le categorie dove fai teoria della computabilità si chiamano categorie di Turing, quelle dove fai teoria dei modelli si chiamano categorie accessibili, quelle dove fai algebra omologica si chiamano Abeliane...

4. Ora, il linguaggio interno di una categoria definisce un sistema di tipi, nel senso della teoria dei tipi, e questo è il motivo in forza del quale ogni categoria fissa una sua propria fondazione della matematica[nota]Storicamente la teoria dei tipi è nata per ovviare alle costruzioni paradossali della teoria degli insiemi, e questo lo sanno tutti; un suo raffinamento fa da fondazione alla matematica, in maniera ugualmente espressiva -ma più "igienica"- della teoria degli insiemi.[/nota]. Infine, un sistema di tipi non è una cosa molto diversa da un linguaggio di programmazione.

Quello che ti ho appena detto, riassumendo una storia molto lunga di cui tra l'altro si parlava proprio qui un annetto fa, è che sono equivalenti i seguenti framework in cui fare matematica:

- la deduzione naturale à la Gentzen;
- il $\lambda$-calcolo à la Church;
- la teoria delle categorie.

5. Voevodsky si è allora chiesto: d'accordo, categoria = posto dove fare matematica = sistema di deduzione naturale tipato = linguaggio di programmazione in cui i programmi sono dimostrazioni dei teoremi provabili nel sistema. Ma allora, siccome esiste una classe di categorie "fatte apposta" per fare topologia algebrica, ossia per ragionare su costruzioni e operazioni valide a meno di omotopia... deve esistere un sistema di tipi fatto apposta per ragionare su costruzioni e operazioni valide a meno di omotopia! Trovarlo non è un puntiglio fondazionale, ma un'urgenza di chiunque necessiti di formalizzare completamente i propri argomenti, per evitare di nascondere errori nel proprio ragionamento.

Tanto più che questo approccio unificante ha delle conseguenze su problemi di emerita natura pratica: come faccio a costruire una infrastruttura che fa girare del codice quanto più possibile "a prova di errore"? Se studi un po' di questo problema ti rendi conto che non è per nulla diverso dal problema di "come faccio a fare una dimostrazione quanto piu possibile esente da errori e salti logici?". Quindi sono proprio queste idee a permettere (una parte del)l'evoluzione superesponenziale in termini di quanto della nostra esistenza, sicurezza e conoscenze deleghiamo a una macchina: anche qui, un esempio tra tanti: https://www.youtube.com/watch?v=4i7KrG1Afbk

Ora, per quanto riguarda questo:

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

Credo di avere raggiunto una comprensione abbastanza varia della matematica in forza di questi interessi, perché come vedi sono dovuto passare dalla teoria della dimostrazione alla topologia algebrica, alla teoria dei modelli e ritorno. Così come ce l'ha fatta un fesso come me, ce l'hanno fatta altri; Voevodsky conosceva a menadito sia gli affari per cui ha preso una medaglia Fields, sia la logica e la storia della matematica dell'ultimo secolo e mezzo. Quindi sì, la risposta è sì.

Ora avrai pazienza, perché non ho il tempo di rileggere bene quel che ho scritto: devo fare una dimostrazione dove questa espressione \[\epsilon U^oV^o \circ TT'(T')^o \varphi U^oV \circ UV\psi(T')^oT' \circ ST \eta\] riduce a una composizione di due isomorfismi; ah, se solo ci fosse un metodo di far fare questa dimostrazione completamente di routine, ovverosia del tutto non istruttiva, uguale a milioni di altre, a una macchina e non a me (che se metto un apice al posto sbagliato, fotto tutta la dimostrazione)!

[megas_archon]

Al resto -proprio perché non c'è fretta di correre da nessuna parte- rispondo domani, abbi pietà, perché qui sono le 3.27am. Non ho dribblato niente, ma come ti ho scritto in pvt, ormai ho un'età, e non riesco a fare matematica di notte.

Però, ti prego, separa in due questo thread. Mi dà proprio fastidio rispondere qui a una cosa che non c'entra nulla.