Sistemele de demonstrație formală dezvăluie ambiguități trecute cu vederea în matematica avansată

Tabel de Linkuri

Rezumat

1. Mulțumiri și Introducere

2. Proprietăți universale

3. Produse în practică

4. Proprietăți universale în geometria algebrică

5. Problema cu utilizarea egalității de către Grothendieck

6. Mai multe despre hărțile "canonice"

7. Izomorfisme canonice în matematica avansată

8. Rezumat și Referințe

Rezumat și Referințe

Deși nu fac nicio afirmație despre erori în literatură sau goluri în argumente care nu pot fi completate după o anumită muncă, susțin că aceste goluri există și că ar putea fi necesară o nouă matematică din partea formalizatorilor pentru a umple aceste goluri într-un mod eficient. Golurile sunt de două tipuri. În primul rând, există problema oamenilor care fac construcții sau demonstrează teoreme care utilizează esențial un model al unui obiect matematic definit până la un izomorfism unic; golul aici este că trebuie verificat că argumentul nu depinde de detaliile explicite ale modelului.

\ Matematicienii sunt conștienți de acest lucru când vine vorba de, să zicem, alegerea unei baze pentru un spațiu vectorial și apoi verificarea că nimic important nu depinde de alegere, sau alegerea unui reprezentant pentru o clasă de echivalență și apoi verificarea că nimic important nu depinde de reprezentant. Cu toate acestea, ei par să fie mai puțin atenți când fac matematică mai avansată, confundând "o" localizare cu "localizarea" sau "un" pullback cu "pullback-ul", și lăsând cititorului detaliile verificării că multe diagrame comută.

\ Un truc util este abuzul simbolului de egalitate, făcându-l să însemne ceva ce nu înseamnă; acest lucru poate păcăli cititorul să creadă că nimic nu trebuie verificat. Uneori, astfel de verificări pot fi surprinzător de dureroase, și poate fi mai ușor să restructurezi un argument matematic decât să faci efectiv aceste verificări. Al doilea tip de gol este problema diferitelor hărți (cum ar fi hărțile de frontieră în secvențe exacte) care sunt considerate "canonice" când, de fapt, nu sunt unice, și există alegeri implicite de semn care sunt făcute.

\ Din păcate, nu este deloc dificil să indicăm exemple explicite în literatură unde un autor nu precizează exact ce convenție folosește când vine vorba de lucruri precum teoria varietăților Shimura sau algebra omologică. Acest lucru pune o povară inutilă pe matematicianul atent (de exemplu Conrad, sau un demonstrator de teoreme computerizat) care încearcă să utilizeze sau să verifice lucrarea. Ambele probleme au apărut în munca mea de formalizare, și mă aștept să apară mai des pe măsură ce intrăm mai adânc în formalizarea matematicii moderne.

Referințe

[AX23] David Kurniadi Angdinata și Junyan Xu, O Demonstrație Formală Elementară a Legii de Grup pe Curbele Eliptice Weierstrass în Orice Caracteristică, A 14-a Conferință Internațională privind Demonstrarea Interactivă a Teoremelor (ITP 2023) (Dagstuhl, Germania) (Adam Naumowicz și René Thiemann, eds.), Leibniz International Proceedings in Informatics (LIPIcs), vol. 268, Schloss Dagstuhl – Leibniz-Zentrum für Informatik, 2023, pp. 6:1– 6:19.

[BCM20] Kevin Buzzard, Johan Commelin, și Patrick Massot, Formalizarea spațiilor perfectoide, Proceedings of the 9th ACM SIGPLAN International Conference on Certified Programs and Proofs, CPP 2020, New Orleans, LA, USA, January 20-21, 2020 (Jasmin Blanchette și Catalin Hritcu, eds.), ACM, 2020, pp. 299–312.

[BPL21] Anthony Bordg, Lawrence Paulson, și Wenda Li, Schemele lui Grothendieck în geometria algebrică, Martie 2021, https://isa-afp.org/entries/Grothendieck_Schemes.html, Dezvoltare formală de demonstrație.

[Buz] Kevin M. Buzzard, Abordarea lui Grothendieck privind egalitatea, https://www.youtube.com/watch?v=-OjCMsqZ9ww, Accesat: 12-08-2023. [Buz19] Buzzard, Kevin, Inversul unei bijecții, 2019, [Online; accesat 12-Aug-2023].

[Con00] Brian Conrad, Dualitatea lui Grothendieck și schimbarea bazei, Lecture Notes in Mathematics, vol. 1750, Springer-Verlag, Berlin, 2000. MR 1804902

[dFF23] María Inés de Frutos-Fernández, Formalizarea Extensiilor de Normă și Aplicații în Teoria Numerelor, A 14-a Conferință Internațională privind Demonstrarea Interactivă a Teoremelor (ITP 2023) (Dagstuhl, Germania) (Adam Naumowicz și René Thiemann, eds.), Leibniz International Proceedings in Informatics (LIPIcs), vol. 268, Schloss Dagstuhl – LeibnizZentrum für Informatik, 2023, pp. 13:1–13:18.

[Gro60] A. Grothendieck, Elemente de geometrie algebrică. I. Limbajul schemelor, Inst. Hautes Etudes Sci. Publ. Math. (1960), no. 4, 228. MR 217083

[Lan97] R. P. Langlands, Reprezentări ale grupurilor algebrice abeliene, Pacific J. Math. (1997), 231–250, Olga Taussky-Todd: in memoriam. MR 1610871

[Liv23] Amelia Livingston, Cohomologia Grupului în Biblioteca Comunității Lean, A 14-a Conferință Internațională privind Demonstrarea Interactivă a Teoremelor (ITP 2023) (Dagstuhl, Germania) (Adam Naumowicz și René Thiemann, eds.), Leibniz International Proceedings in Informatics (LIPIcs), vol. 268, Schloss Dagstuhl – Leibniz-Zentrum für Informatik, 2023, pp. 22:1–22:17.

[mC20] Comunitatea mathlib, Biblioteca matematică lean, Proceedings of the 9th ACM SIGPLAN International Conference on Certified Programs and Proofs, ACM, ian 2020.

[Mil80] James S. Milne, Cohomologie étale, Princeton Mathematical Series, No. 33, Princeton University Press, Princeton, N.J., 1980. MR 559531

[Sta18] Autorii Proiectului Stacks, Proiectul Stacks, https://stacks.math.columbia.edu, 2018.

[Wei59] André Weil, Corespondență [semnată "R. Lipschitz"], Ann. of Math. (2) 69 (1959), 247–251, Atribuită lui A. Weil. MR 100637 [Wik04a] Contribuitori Wikipedia, Categorie monoidală — Wikipedia, enciclopedia liberă, 2004, [Online; accesat 12-Aug-2023].

[Wik04b] , Pereche ordonată — Wikipedia, enciclopedia liberă, 2004, [Online; accesat 20-Mai-2023].

[Zha23] Jujian Zhang, Formalizarea Construcției Proj în Lean, A 14-a Conferință Internațională privind Demonstrarea Interactivă a Teoremelor (ITP 2023) (Dagstuhl, Germania) (Adam Naumowicz și René Thiemann, eds.), Leibniz International Proceedings in Informatics (LIPIcs), vol. 268, Schloss Dagstuhl – Leibniz-Zentrum für Informatik, 2023, pp. 35:1– 35:17.

[ZM23] Max Zeuner și Anders Mörtberg, O formalizare univalentă a schemelor afine constructive, 2023. Adresă de email: k.buzzard@imperial.ac.uk Departamentul de Matematică, Imperial College London

:::info Autor: KEVIN BUZZARD

:::

:::info Această lucrare este disponibilă pe arxiv sub licența CC BY 4.0 DEED.

:::

\