Los sistemas formales de demostración revelan ambigüedades pasadas por alto en matemáticas avanzadas

Tabla De Enlaces

Resumen

1. Agradecimientos e Introducción

2. Propiedades universales

3. Productos en la práctica

4. Propiedades universales en geometría algebraica

5. El problema con el uso de igualdad de Grothendieck

6. Más sobre mapas "canónicos"

7. Isomorfismos canónicos en matemáticas más avanzadas

8. Resumen y Referencias

Resumen y Referencias

Aunque no estoy haciendo ninguna afirmación sobre errores en la literatura o vacíos en argumentos que no puedan ser completados después de algún trabajo, sostengo que estos vacíos existen, y que podría ser necesario desarrollar nueva matemática por parte de los formalizadores para llenar estos vacíos de manera eficiente. Los vacíos son de dos tipos. Primero está el problema de personas que hacen construcciones o demuestran teoremas que hacen uso esencial de un modelo de un objeto matemático que está definido hasta un isomorfismo único; el vacío aquí es que se necesita verificar que el argumento no depende de los detalles explícitos del modelo.

\ Los matemáticos son muy conscientes de esto cuando se trata de, por ejemplo, elegir una base para un espacio vectorial y luego verificar que nada importante dependía de la elección, o elegir un representante para una clase de equivalencia y luego verificar que nada importante depende del representante. Sin embargo, parecen ser menos cuidadosos al hacer matemáticas más avanzadas, confundiendo "una" localización con "la" localización o "un" pullback con "el" pullback, y dejando al lector los detalles de verificar que muchos diagramas conmutan.

\ Un truco útil es abusar del símbolo de igualdad, haciéndolo significar algo que no significa; esto puede engañar al lector haciéndole pensar que no hay nada que verificar. A veces, tales verificaciones pueden ser sorprendentemente dolorosas, y puede ser más fácil reestructurar un argumento matemático que hacer realmente estas verificaciones. El segundo tipo de vacío es el problema de varios mapas (como mapas de frontera en secuencias exactas) que se consideran "canónicos" cuando en realidad no son únicos, y se están haciendo elecciones implícitas de signo.

\ Desafortunadamente, no es difícil señalar ejemplos explícitos en la literatura donde un autor no indica precisamente qué convención está utilizando cuando se trata de cosas como la teoría de variedades de Shimura, o álgebra homológica. Esto impone una carga innecesaria al matemático cuidadoso (por ejemplo, Conrad, o un demostrador de teoremas por computadora) que está intentando usar o verificar el trabajo. Ambos problemas han aparecido en mi trabajo de formalización, y espero que aparezcan con más frecuencia a medida que profundizamos en la formalización de las matemáticas modernas.

Referencias

[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 Este artículo está disponible en arxiv bajo la licencia CC BY 4.0 DEED.

:::

\