Formalne systemy dowodzenia ujawniają przeoczone niejednoznaczności w zaawansowanej matematyce

Spis linków

Abstrakt

1. Podziękowania i wprowadzenie

2. Własności uniwersalne

3. Produkty w praktyce

4. Własności uniwersalne w geometrii algebraicznej

5. Problem z użyciem równości przez Grothendiecka

6. Więcej o "kanonicznych" odwzorowaniach

7. Kanoniczne izomorfizmy w bardziej zaawansowanej matematyce

8. Podsumowanie i bibliografia

Podsumowanie i bibliografia

Chociaż nie twierdzę, że istnieją błędy w literaturze lub luki w argumentacji, których nie można wypełnić po pewnej pracy, argumentuję, że te luki istnieją i że nowa matematyka może być potrzebna formalizatorom, aby wypełnić te luki w sposób efektywny. Luki są dwojakiego rodzaju. Po pierwsze, istnieje problem ludzi tworzących konstrukcje lub dowodzących twierdzeń, które istotnie wykorzystują model obiektu matematycznego zdefiniowanego z dokładnością do jednoznacznego izomorfizmu; luką jest tutaj to, że należy sprawdzić, czy argument nie zależy od szczegółów modelu.

\ Matematycy są tego świadomi, gdy chodzi o, powiedzmy, wybór bazy dla przestrzeni wektorowej, a następnie sprawdzenie, że nic ważnego nie zależało od wyboru, lub wybór reprezentanta klasy równoważności, a następnie sprawdzenie, że nic ważnego nie zależy od reprezentanta. Jednak wydają się być mniej ostrożni przy wykonywaniu bardziej zaawansowanej matematyki, myląc "jakąś" lokalizację z "tą" lokalizacją lub "jakiś" pullback z "tym" pullbackiem, pozostawiając czytelnikowi szczegóły sprawdzania, że wiele diagramów jest przemiennych.

\ Jednym z użytecznych trików jest nadużywanie symbolu równości, sprawiając, że oznacza coś, czego nie oznacza; może to zmylić czytelnika, myślącego, że nic nie trzeba sprawdzać. Czasami takie sprawdzenia mogą być zaskakująco bolesne i może być łatwiej przebudować argument matematyczny niż faktycznie dokonać tych sprawdzeń. Drugi rodzaj luki to kwestia różnych odwzorowań (jak odwzorowania brzegowe w dokładnych ciągach) uważanych za "kanoniczne", podczas gdy w rzeczywistości nie są one jednoznaczne, a dokonywane są niejawne wybory znaku.

\ Niestety, nie jest trudno wskazać konkretne przykłady w literaturze, gdzie autor nie określa dokładnie, jakiej konwencji używa, gdy chodzi o takie rzeczy jak teoria rozmaitości Shimury czy algebra homologiczna. Nakłada to niepotrzebne obciążenie na uważnego matematyka (na przykład Conrada lub komputerowy program dowodzący twierdzeń), który próbuje wykorzystać lub zweryfikować pracę. Oba te problemy pojawiły się w mojej pracy formalizacyjnej i spodziewam się, że będą pojawiać się częściej, gdy będziemy zagłębiać się w formalizację współczesnej matematyki.

Bibliografia

[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: k.buzzard@imperial.ac.uk Department of Mathematics, Imperial College London

:::info Autor: KEVIN BUZZARD

:::

:::info Ten artykuł jest dostępny na arxiv na licencji CC BY 4.0 DEED.

:::

\