Formele Bewijssystemen Onthullen Over het Hoofd Geziene Dubbelzinnigheden in Geavanceerde Wiskunde

Tabel Van Links

Abstract

1. Dankwoord & Inleiding

2. Universele eigenschappen

3. Producten in de praktijk

4. Universele eigenschappen in algebraïsche meetkunde

5. Het probleem met Grothendieck's gebruik van gelijkheid

6. Meer over "canonieke" afbeeldingen

7. Canonieke isomorfismen in meer geavanceerde wiskunde

8. Samenvatting En Referenties

Samenvatting En Referenties

Hoewel ik geen beweringen doe over fouten in de literatuur of gaten in argumenten die niet kunnen worden opgevuld na enig werk, betoog ik dat deze gaten wel bestaan, en dat nieuwe wiskunde mogelijk moet worden gedaan door formaliseerders om deze gaten op een efficiënte manier op te vullen. De gaten zijn van twee soorten. Ten eerste is er het probleem van mensen die constructies maken of stellingen bewijzen die essentieel gebruik maken van een model van een wiskundig object dat tot op uniek isomorfisme is gedefinieerd; het gat hier is dat gecontroleerd moet worden dat het argument niet afhangt van de expliciete details van het model.

\ Wiskundigen zijn zich hiervan goed bewust als het gaat om, bijvoorbeeld, het kiezen van een basis voor een vectorruimte en dan controleren dat niets belangrijks afhing van de keuze, of het kiezen van een representant voor een equivalentieklasse en dan controleren dat niets belangrijks afhangt van de representant. Ze lijken echter minder zorgvuldig te zijn bij het doen van meer geavanceerde wiskunde, waarbij ze "een" lokalisatie verwarren met "de" lokalisatie of "een" pullback met "de" pullback, en aan de lezer de details overlaten van het controleren dat veel diagrammen commuteren.

\ Een nuttige truc is om het gelijkheidssymbool te misbruiken, door het iets te laten betekenen wat het niet betekent; dit kan de lezer misleiden door te denken dat er niets gecontroleerd hoeft te worden. Soms kunnen dergelijke controles verrassend pijnlijk zijn, en kan het gemakkelijker zijn om een wiskundig argument te herstructureren dan om deze controles daadwerkelijk uit te voeren. De tweede soort gat is het probleem van verschillende afbeeldingen (zoals randafbeeldingen in exacte rijtjes) die worden beschouwd als "canoniek" terwijl ze in feite niet uniek zijn, en er impliciete keuzes van teken worden gemaakt.

\ Helaas is het niet moeilijk om expliciete voorbeelden in de literatuur aan te wijzen waar een auteur niet precies aangeeft welke conventie ze gebruiken als het gaat om zaken als de theorie van Shimura-variëteiten, of homologische algebra. Dit legt een onnodige last op de zorgvuldige wiskundige (bijvoorbeeld Conrad, of een computerbewijsassistent) die probeert het werk te gebruiken of te verifiëren. Beide kwesties zijn naar voren gekomen in mijn formalisatiewerk, en ik verwacht dat ze vaker zullen voorkomen naarmate we dieper ingaan op de formalisatie van moderne wiskunde.

Referenties

[AX23] David Kurniadi Angdinata and Junyan Xu, An Elementary Formal Proof of the Group Law on Weierstrass Elliptic Curves in Any Characteristic, 14th International Conference on Interactive Theorem Proving (ITP 2023) (Dagstuhl, Germany) (Adam Naumowicz and Ren´e Thiemann, eds.), Leibniz International Proceedings in Informatics (LIPIcs), vol. 268, Schloss Dagstuhl – Leibniz-Zentrum f¨ur Informatik, 2023, pp. 6:1– 6:19.

[BCM20] Kevin Buzzard, Johan Commelin, and Patrick Massot, Formalising perfectoid spaces, 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 and Catalin Hritcu, eds.), ACM, 2020, pp. 299–312.

[BPL21] Anthony Bordg, Lawrence Paulson, and Wenda Li, Grothendieck's schemes in algebraic geometry, March 2021, https://isa-afp.org/entries/Grothendieck_Schemes.html, Formal proof development.

[Buz] Kevin M. Buzzard, Grothendieck's approach to equality, https://www.youtube.com/watch?v=-OjCMsqZ9ww, Accessed: 12-08-2023. [Buz19] Buzzard, Kevin, The inverse of a bijection, 2019, [Online; accessed 12-Aug-2023].

[Con00] Brian Conrad, Grothendieck duality and base change, Lecture Notes in Mathematics, vol. 1750, Springer-Verlag, Berlin, 2000. MR 1804902

[dFF23] Mar´ıa In´es de Frutos-Fern´andez, Formalizing Norm Extensions and Applications to Number Theory, 14th International Conference on Interactive Theorem Proving (ITP 2023) (Dagstuhl, Germany) (Adam Naumowicz and Ren´e Thiemann, eds.), Leibniz International Proceedings in Informatics (LIPIcs), vol. 268, Schloss Dagstuhl – LeibnizZentrum f¨ur Informatik, 2023, pp. 13:1–13:18.

[Gro60] A. Grothendieck, El´ements de g´eom´etrie alg´ebrique. I. Le langage des sch ´ ´emas, Inst. Hautes Etudes Sci. Publ. Math. (1960), no. 4, 228. MR 217083 ´

[Lan97] R. P. Langlands, Representations of abelian algebraic groups, Pacific J. Math. (1997), 231–250, Olga Taussky-Todd: in memoriam. MR 1610871

[Liv23] Amelia Livingston, Group Cohomology in the Lean Community Library, 14th International Conference on Interactive Theorem Proving (ITP 2023) (Dagstuhl, Germany) (Adam Naumowicz and Ren´e Thiemann, eds.), Leibniz International Proceedings in Informatics (LIPIcs), vol. 268, Schloss Dagstuhl – Leibniz-Zentrum f¨ur Informatik, 2023, pp. 22:1–22:17.

[mC20] The mathlib Community, The lean mathematical library, Proceedings of the 9th ACM SIGPLAN International Conference on Certified Programs and Proofs, ACM, jan 2020.

[Mil80] James S. Milne, Etale cohomology ´ , Princeton Mathematical Series, No. 33, Princeton University Press, Princeton, N.J., 1980. MR 559531

[Sta18] The Stacks Project Authors, Stacks Project, https://stacks.math.columbia.edu, 2018.

[Wei59] Andr´e Weil, Correspondence [signed "R. Lipschitz"], Ann. of Math. (2) 69 (1959), 247–251, Attributed to A. Weil. MR 100637 [Wik04a] Wikipedia contributors, Monoidal category — Wikipedia, the free encyclopedia, 2004, [Online; accessed 12-Aug-2023].

[Wik04b] , Ordered pair — Wikipedia, the free encyclopedia, 2004, [Online; accessed 20- May-2023].

[Zha23] Jujian Zhang, Formalising the Proj Construction in Lean, 14th International Conference on Interactive Theorem Proving (ITP 2023) (Dagstuhl, Germany) (Adam Naumowicz and Ren´e Thiemann, eds.), Leibniz International Proceedings in Informatics (LIPIcs), vol. 268, Schloss Dagstuhl – Leibniz-Zentrum f¨ur Informatik, 2023, pp. 35:1– 35:17.

[ZM23] Max Zeuner and Anders M¨ortberg, A univalent formalization of constructive affine schemes, 2023. Email address: [email protected] Department of Mathematics, Imperial College London

:::info Auteur: KEVIN BUZZARD

:::

:::info Dit artikel is beschikbaar op arxiv onder CC BY 4.0 DEED licentie.

:::

\