形式的証明システムが高度数学における見過ごされた曖昧さを明らかにする

リンク一覧

概要

1. 謝辞と序論

2. 普遍的性質

3. 実践における積

4. 代数幾何学における普遍的性質

5. グロタンディークの等号の使用に関する問題

6. 「標準的な」写像についての詳細

7. より高度な数学における標準的同型

8. 概要と参考文献

概要と参考文献

私は文献中の誤りや、ある程度の作業後に埋められない議論の穴について主張しているわけではありませんが、これらの穴が存在し、形式化者がこれらの穴を効率的に埋めるために新しい数学が必要になるかもしれないと主張しています。穴は二種類あります。まず、一意的な同型まで定義される数学的対象のモデルを本質的に使用する構成や定理の証明を行う人々の問題があります。ここでの穴は、その議論がモデルの明示的な詳細に依存しないことを確認する必要があるということです。

\ 数学者は、例えばベクトル空間の基底を選び、その選択に重要なものが依存していないことを確認したり、同値類の代表元を選び、その代表元に重要なものが依存していないことを確認したりする場合、これをよく認識しています。しかし、より高度な数学を行う際には、「ある」局所化と「その」局所化、または「ある」引き戻しと「その」引き戻しを混同し、多くの図式が可換であることを確認する詳細を読者に委ねるなど、あまり注意を払っていないようです。

\ 一つの便利なトリックは、等号記号を乱用し、それが意味しないものを意味させることです。これにより、何も確認する必要がないと読者に思わせることができます。時にはそのような確認が驚くほど苦痛であり、実際にこれらの確認を行うよりも数学的議論を再構成する方が容易な場合があります。二番目の種類の穴は、（完全列における境界写像のような）様々な写像が「標準的」とみなされる問題で、実際には一意ではなく、符号の暗黙的な選択が行われています。

\ 残念ながら、志村多様体の理論や、ホモロジー代数などに関して、著者が正確にどの規約を使用しているかを明記していない文献中の明示的な例を指摘することは全く難しくありません。これは、その作業を使用または検証しようとしている注意深い数学者（例えばコンラッドやコンピュータ定理証明器）に不必要な負担をかけます。これらの問題は私の形式化作業で現れており、現代数学の形式化がより深まるにつれて、より頻繁に現れると予想しています。

参考文献

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

:::

:::info この論文は arxivで入手可能 であり、CC BY 4.0 DEEDライセンスの下で公開されています。

:::

\