Sistemas de Prova Formal Revelam Ambiguidades Negligenciadas na Matemática Avançada

Tabela De Links

Resumo

1. Agradecimentos e Introdução

2. Propriedades universais

3. Produtos na prática

4. Propriedades universais em geometria algébrica

5. O problema com o uso de igualdade de Grothendieck

6. Mais sobre mapas "canônicos"

7. Isomorfismos canônicos em matemática mais avançada

8. Resumo e Referências

Resumo e Referências

Embora eu não esteja fazendo nenhuma afirmação sobre erros na literatura ou lacunas em argumentos que não possam ser preenchidas após algum trabalho, estou argumentando que essas lacunas existem, e que nova matemática pode precisar ser feita por formalizadores para preencher essas lacunas de maneira eficiente. As lacunas são de dois tipos. Primeiro, há a questão de pessoas fazendo construções ou provando teoremas que fazem uso essencial de um modelo de um objeto matemático que é definido até isomorfismo único; a lacuna aqui é que precisa ser verificado que o argumento não depende dos detalhes explícitos do modelo.

\ Os matemáticos estão bem cientes disso quando se trata de, por exemplo, escolher uma base para um espaço vetorial e depois verificar que nada importante dependia da escolha, ou escolher um representante para uma classe de equivalência e depois verificar que nada importante depende do representante. No entanto, eles parecem ser menos cuidadosos ao fazer matemática mais avançada, confundindo "uma" localização com "a" localização ou "um" pullback com "o" pullback, e deixando para o leitor os detalhes de verificar que muitos diagramas comutam.

\ Um truque útil é abusar do símbolo de igualdade, fazendo-o significar algo que não significa; isso pode enganar o leitor a pensar que nada precisa ser verificado. Às vezes, tais verificações podem ser surpreendentemente dolorosas, e pode ser mais fácil reestruturar um argumento matemático do que realmente fazer essas verificações. O segundo tipo de lacuna é a questão de vários mapas (como mapas de fronteira em sequências exatas) serem considerados "canônicos" onde agora eles de fato não são únicos, e há escolhas implícitas de sinal sendo feitas.

\ Infelizmente, não é nada difícil apontar exemplos explícitos na literatura onde um autor não declara precisamente qual convenção está usando quando se trata de coisas como a teoria das variedades de Shimura, ou álgebra homológica. Isso coloca um fardo desnecessário sobre o matemático cuidadoso (por exemplo, Conrad, ou um provador de teoremas por computador) que está tentando usar ou verificar o trabalho. Ambas essas questões apareceram no meu trabalho de formalização, e espero que apareçam com mais frequência à medida que aprofundamos a formalização da matemática moderna.

Referências

[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 artigo está disponível no arxiv sob licença CC BY 4.0 DEED.

:::

\