形式化證明系統揭示高等數學中被忽視的歧義

連結目錄

摘要

1. 致謝與引言

2. 普適性質

3. 實踐中的積

4. 代數幾何中的普適性質

5. Grothendieck 使用等式的問題

6. 關於「典範」映射的更多討論

7. 更高等數學中的典範同構

8. 總結與參考文獻

總結與參考文獻

雖然我並不聲稱文獻中存在無法經過一些工作填補的錯誤或論證中的漏洞，但我確實認為這些漏洞存在，並且形式化工作者可能需要創造新的數學來有效地填補這些漏洞。這些漏洞有兩種類型。首先是人們在構造或證明定理時，本質上使用了一個數學對象的模型，而該模型僅在唯一同構下被定義；這裡的漏洞是需要檢查論證不依賴於模型的明確細節。

\ 數學家在選擇向量空間的基底然後檢查沒有重要的東西依賴於這個選擇，或選擇等價類的代表然後檢查沒有重要的東西依賴於這個代表時，都很清楚這一點。然而，在進行更高等的數學時，他們似乎不那麼謹慎，混淆了「一個」局部化與「那個」局部化，或「一個」拉回與「那個」拉回，並將檢查許多圖表交換的細節留給讀者。

\ 一個有用的技巧是濫用等號，使其表示它本不該表示的意思；這可能會誤導讀者認為不需要進行任何檢查。有時這些檢查可能出乎意料地痛苦，重構數學論證可能比實際進行這些檢查更容易。第二種類型的漏洞是各種映射（如精確序列中的邊界映射）被視為「典範的」，而實際上它們並非唯一，並且存在隱含的符號選擇。

\ 不幸的是，在文獻中指出明確的例子並不困難，其中作者在涉及 Shimura 簇理論或同調代數等事物時，並未精確說明他們使用的慣例。這給試圖使用或驗證這項工作的謹慎數學家（例如 Conrad 或計算機定理證明器）帶來了不必要的負擔。這兩個問題都在我的形式化工作中出現過，我預期隨著我們深入現代數學的形式化，它們會更頻繁地出現。

參考文獻

[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 許可證。

:::

\