Les systèmes de preuve formelle révèlent des ambiguïtés négligées dans les mathématiques avancées

Table Des Liens

Résumé

1. Remerciements & Introduction

2. Propriétés universelles

3. Produits en pratique

4. Propriétés universelles en géométrie algébrique

5. Le problème avec l'utilisation de l'égalité par Grothendieck

6. Plus sur les applications "canoniques"

7. Isomorphismes canoniques dans les mathématiques plus avancées

8. Aperçu et Références

Aperçu et Références

Bien que je ne prétende pas qu'il y ait des erreurs dans la littérature ou des lacunes dans les arguments qui ne peuvent être comblées après un certain travail, je soutiens que ces lacunes existent, et que de nouvelles mathématiques pourraient devoir être développées par les formalisateurs afin de combler ces lacunes de manière efficace. Les lacunes sont de deux types. Premièrement, il y a le problème des personnes qui font des constructions ou prouvent des théorèmes qui utilisent essentiellement un modèle d'un objet mathématique défini à isomorphisme unique près ; la lacune ici est qu'il faut vérifier que l'argument ne dépend pas des détails explicites du modèle.

\ Les mathématiciens sont bien conscients de cela lorsqu'il s'agit, par exemple, de choisir une base pour un espace vectoriel puis de vérifier qu'aucun élément important ne dépendait de ce choix, ou de choisir un représentant pour une classe d'équivalence puis de vérifier qu'aucun élément important ne dépend du représentant. Cependant, ils semblent être moins prudents lorsqu'ils font des mathématiques plus avancées, confondant "une" localisation avec "la" localisation ou "un" pullback avec "le" pullback, et laissant au lecteur les détails de la vérification que de nombreux diagrammes commutent.

\ Une astuce utile consiste à abuser du symbole d'égalité, en lui faisant signifier quelque chose qu'il ne signifie pas ; cela peut tromper le lecteur en lui faisant croire que rien n'a besoin d'être vérifié. Parfois, de telles vérifications peuvent être étonnamment pénibles, et il peut être plus facile de restructurer un argument mathématique que de faire réellement ces vérifications. Le deuxième type de lacune est le problème de diverses applications (comme les applications de bord dans les séquences exactes) considérées comme "canoniques" alors qu'elles ne sont en fait pas uniques, et qu'il y a des choix implicites de signe qui sont faits.

\ Malheureusement, il n'est pas du tout difficile de pointer des exemples explicites dans la littérature où un auteur ne précise pas exactement quelle convention il utilise lorsqu'il s'agit de choses comme la théorie des variétés de Shimura, ou l'algèbre homologique. Cela impose une charge inutile au mathématicien minutieux (par exemple Conrad, ou un démonstrateur de théorèmes informatique) qui tente d'utiliser ou de vérifier le travail. Ces deux problèmes sont apparus dans mon travail de formalisation, et je m'attends à ce qu'ils apparaissent plus souvent à mesure que nous approfondissons la formalisation des mathématiques modernes.

Références

[AX23] David Kurniadi Angdinata et 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, et 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, et 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, Consulté le : 12-08-2023. [Buz19] Buzzard, Kevin, The inverse of a bijection, 2019, [En ligne; consulté le 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, [En ligne; consulté le 12-Aug-2023].

[Wik04b] , Ordered pair — Wikipedia, the free encyclopedia, 2004, [En ligne; consulté le 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 et Anders M¨ortberg, A univalent formalization of constructive affine schemes, 2023. Adresse e-mail : [email protected] Department of Mathematics, Imperial College London

:::info Auteur : KEVIN BUZZARD

:::

:::info Cet article est disponible sur arxiv sous licence CC BY 4.0 DEED.

:::

\