Progetti di testo di base online, in evoluzione e collaborativi
Ci sono due progetti di "testo fondamentale" online, in evoluzione e collaborativi per matematici di ricerca di cui sono a conoscenza:
(1) Il progetto Stacks per la geometria algebrica
(2) Kerodon per la teoria dell'omotopia categoriale
Sono una specie di Bourbaki per l'era di Internet. Vorrei sapere se ce ne sono altri della stessa natura in corso o in vista.
Si prega di notare che non sto cercando testi o monografie disponibili online, motivo per cui ho evidenziato gli aggettivi nella prima riga.
Risposte
Mathlib è un progetto online, in evoluzione e collaborativo, che mira a essere una base per tutta la moderna matematica pura. E ' completamente ricercabile , ed ecco la sua homepage . È ospitato su github ed è tutto verificato con il Lean Theorem Prover.
Un ottimo posto per vedere lo stato attuale di mathlib è questa pagina panoramica , che la comunità tiene aggiornata.
Ci sono ancora alcune parti della matematica universitaria non coperte da mathlib, ma d'altra parte c'è molta matematica avanzata lì; ad esempio, i risultati recenti (2020) includono un gruppo di algebra commutativa di livello MSc (ad es. DVR ), un inizio sull'algebra omologica , algebre di Lie , un gruppo di teoria della misura astratta e misura di Haar , varietà e fasci . Tuttavia, il mio elenco diventerà presto obsoleto: controlla la pagina della panoramica per i risultati recenti.
Finora hanno contribuito circa 100 persone, dai ragazzi delle scuole superiori ai professori ordinari (in particolare è genuinamente collaborativo); tutto quello che devi fare è imparare il linguaggio di programmazione Lean in modo da poter esprimere la matematica in Lean, e poi formalizzare qualcosa che vogliamo nella libreria. Accogliamo con favore contributi da molte aree della matematica - oltre al materiale standard UG e MSc in teoria dei numeri, geometria, topologia, analisi e algebra, c'è la teoria dei giochi combinatoria, la geometria euclidea e molte altre cose. Ecco un elenco di materiale di livello universitario che ancora non abbiamo.
Tre anni fa la biblioteca non aveva praticamente nulla (niente numeri complessi, niente seno e coseno, per esempio). Ma sta crescendo rapidamente e la mia convinzione personale è che alla fine sia un modo più moderno di presentare la matematica rispetto allo Stacks Project e al Kerodon. Nei prossimi anni, se tutto andrà bene, parte di mathlib si integrerà con lo Stacks Project; sia le persone di mathlib che quelle del progetto stacks sono interessate alla collaborazione, e questo recente PR di Scott Morrison(uno dei fondatori di MathOverflow!) è un altro trampolino di lancio verso gli schemi; dovremmo averli in mathlib entro le prossime settimane (esistono già nel codice Lean ma abbiamo imparato a nostre spese che le cose non in mathlib sono soggette a bitrot). Il motivo per cui penso che mathlib alla fine sarà più importante del progetto Stacks o Kerodon è che mathlib è leggibile dalla macchina, consentendo ai computer di leggere la matematica a livello di ricerca. Sfortunatamente i computer non sono ancora in grado di comprendere il linguaggio naturale, il che significa che è difficile per l'intelligenza artificiale utilizzare ad esempio ArXiv per fare matematica a livello di ricerca, quindi in questo momento mi sembra che la formalizzazione sia un modo naturale di procedere. Credo che sia inevitabile che un giorno le macchine facciano bene la matematica, così come era inevitabile che un giorno giocassero a scacchi e andassero bene;
Le persone interessate a contribuire possono dare un'occhiata alla chat Zulip : si tratta di una chat room mirata in cui le persone usano i loro veri nomi e gli esperti lavorano su questioni che sono emerse dalla formalizzazione della matematica. A volte ci sono 1000 post in un giorno e gran parte della conversazione è altamente tecnica, ma c'è un #new membersflusso in cui i principianti possono porre domande. Si prega di leggere le linee guida della community . In breve: sii gentile. E 'così semplice.
I matematici che desiderano imparare qualcosa su come contribuire potrebbero trovare interessanti i video di YouTube del workshop introduttivo del mese scorso Lean for the curioso matematico . C'è anche il libro in corso Mathematics in Lean .
Non direi che Kerodon è collaborativo, ma perché il$n$Lab non è nella lista?
Personalmente citerei due libri:
La "Geometria differenziale ricostruita" di Kenningtonhttp://www.geometry.org/tex/conc/dgstats.phpl'autore sviluppa tutto in modo molto dettagliato dall'inizio, e per "inizio" intendo le sue opinioni personali su metamatematica, logica dei predicati, calcolo sequenziale, algebra, analisi e tutta la topologia che vedrai/necessario.
L'ultima versione di "Fondamenti della teoria quasi dell'anello"https://arxiv.org/abs/math/0409584dove gli autori prendono personalmente l'assenza di un libro di testo completo sulla teoria delle 2 categorie.
Un progetto estremamente entusiasmante appartenente a questa lista è Automorphic Project di Yiannis Sakellaridis !
Per la teoria dei numeri, c'è questo progetto molto interessante simile al progetto Stacks che sembra coprire in modo molto dettagliato tutti i principali sottocampi della moderna teoria dei numeri:
https://github.com/holdenlee/number-theory