I Sistemi di Dimostrazione Formale Rivelano Ambiguità Trascurate nella Matematica Avanzata

Tabella Dei Link

Abstract

1. Ringraziamenti e Introduzione

2. Proprietà universali

3. Prodotti in pratica

4. Proprietà universali in geometria algebrica

5. Il problema con l'uso dell'uguaglianza di Grothendieck

6. Altro sulle mappe "canoniche"

7. Isomorfismi canonici nella matematica più avanzata

8. Riepilogo e Riferimenti

Riepilogo e Riferimenti

Sebbene non stia facendo alcuna affermazione su errori nella letteratura o lacune negli argomenti che non possono essere colmate dopo un po' di lavoro, sostengo che queste lacune esistano e che potrebbe essere necessario sviluppare nuova matematica da parte dei formalizzatori per colmare queste lacune in modo efficiente. Le lacune sono di due tipi. In primo luogo, c'è il problema delle persone che fanno costruzioni o dimostrano teoremi che fanno uso essenziale di un modello di un oggetto matematico che è definito a meno di un isomorfismo unico; la lacuna qui è che deve essere verificato che l'argomento non dipenda dai dettagli espliciti del modello.

\ I matematici sono ben consapevoli di questo quando si tratta, ad esempio, di scegliere una base per uno spazio vettoriale e poi verificare che nulla di importante dipendesse dalla scelta, o di scegliere un rappresentante per una classe di equivalenza e poi verificare che nulla di importante dipenda dal rappresentante. Tuttavia, sembrano essere meno attenti quando fanno matematica più avanzata, confondendo "una" localizzazione con "la" localizzazione o "un" pullback con "il" pullback, e lasciando al lettore i dettagli della verifica che molti diagrammi commutino.

\ Un trucco utile è abusare del simbolo di uguaglianza, facendogli significare qualcosa che non significa; questo può ingannare il lettore facendogli pensare che non ci sia nulla da verificare. A volte tali verifiche possono essere sorprendentemente dolorose, e può essere più facile ristrutturare un argomento matematico piuttosto che effettuare queste verifiche. Il secondo tipo di lacuna è la questione di varie mappe (come le mappe di confine nelle sequenze esatte) considerate come "canoniche" quando in realtà non sono uniche, e ci sono scelte implicite di segno che vengono fatte.

\ Sfortunatamente, non è affatto difficile indicare esempi espliciti nella letteratura in cui un autore non dichiara precisamente quale convenzione sta usando quando si tratta di cose come la teoria delle varietà di Shimura, o l'algebra omologica. Questo pone un onere inutile sul matematico attento (per esempio Conrad, o un dimostratore di teoremi computerizzato) che sta cercando di utilizzare o verificare il lavoro. Entrambi questi problemi sono emersi nel mio lavoro di formalizzazione, e mi aspetto che emergano più spesso man mano che approfondiamo la formalizzazione della matematica moderna.

Riferimenti

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

:::

:::info Questo documento è disponibile su arxiv sotto licenza CC BY 4.0 DEED.

:::

\