Formale Beweissysteme decken übersehene Mehrdeutigkeiten in der höheren Mathematik auf

Inhaltsverzeichnis

Abstrakt

1. Danksagungen & Einleitung

2. Universelle Eigenschaften

3. Produkte in der Praxis

4. Universelle Eigenschaften in der algebraischen Geometrie

5. Das Problem mit Grothendiecks Verwendung der Gleichheit

6. Mehr über "kanonische" Abbildungen

7. Kanonische Isomorphismen in fortgeschrittener Mathematik

8. Zusammenfassung und Referenzen

Zusammenfassung und Referenzen

Obwohl ich keine Behauptungen über Fehler in der Literatur oder Lücken in Argumenten aufstelle, die nach einiger Arbeit nicht gefüllt werden können, argumentiere ich, dass diese Lücken existieren und dass neue Mathematik von Formalisierern entwickelt werden muss, um diese Lücken effizient zu füllen. Die Lücken sind zweierlei Art. Erstens gibt es das Problem, dass Menschen Konstruktionen erstellen oder Theoreme beweisen, die wesentlich ein Modell eines mathematischen Objekts verwenden, das bis auf eindeutigen Isomorphismus definiert ist; die Lücke besteht darin, dass überprüft werden muss, ob das Argument nicht von den expliziten Details des Modells abhängt.

\ Mathematiker sind sich dessen bewusst, wenn es darum geht, beispielsweise eine Basis für einen Vektorraum zu wählen und dann zu überprüfen, dass nichts Wichtiges von der Wahl abhängt, oder einen Repräsentanten für eine Äquivalenzklasse zu wählen und dann zu überprüfen, dass nichts Wichtiges vom Repräsentanten abhängt. Allerdings scheinen sie weniger sorgfältig zu sein, wenn sie fortgeschrittenere Mathematik betreiben, verwechseln "eine" Lokalisierung mit "der" Lokalisierung oder "ein" Pullback mit "dem" Pullback und überlassen dem Leser die Details der Überprüfung, dass viele Diagramme kommutieren.

\ Ein nützlicher Trick besteht darin, das Gleichheitszeichen zu missbrauchen, indem man es etwas bedeuten lässt, was es nicht bedeutet; dies kann den Leser in die Irre führen, dass nichts überprüft werden muss. Manchmal können solche Überprüfungen überraschend schmerzhaft sein, und es kann einfacher sein, ein mathematisches Argument umzustrukturieren, als diese Überprüfungen tatsächlich durchzuführen. Die zweite Art von Lücke ist das Problem verschiedener Abbildungen (wie Randabbildungen in exakten Sequenzen), die als "kanonisch" betrachtet werden, obwohl sie tatsächlich nicht eindeutig sind, und es werden implizite Vorzeichenwahlen getroffen.

\ Leider ist es nicht schwierig, explizite Beispiele in der Literatur zu finden, in denen ein Autor nicht genau angibt, welche Konvention er verwendet, wenn es um Dinge wie die Theorie der Shimura-Varietäten oder homologische Algebra geht. Dies belastet den sorgfältigen Mathematiker (zum Beispiel Conrad oder einen computergestützten Theorembeweiser) unnötig, der versucht, die Arbeit zu verwenden oder zu verifizieren. Beide Probleme sind in meiner Formalisierungsarbeit aufgetreten, und ich erwarte, dass sie häufiger auftreten werden, je tiefer wir in die Formalisierung der modernen Mathematik eindringen.

Referenzen

[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 Autor: KEVIN BUZZARD

:::

:::info Dieses Paper ist auf arxiv verfügbar unter der CC BY 4.0 DEED Lizenz.

:::

\