形式证明系统揭示高等数学中被忽视的歧义

链接目录

摘要

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: [email protected] Department of Mathematics, Imperial College London

:::info 作者： KEVIN BUZZARD

:::

:::info 本论文可在arxiv上获取，采用CC BY 4.0 DEED许可证。

:::

\