Sistem Bukti Formal Mengungkap Ambiguitas yang Terlewatkan dalam Matematika Tingkat Lanjut

Tabel Tautan

Abstrak

1. Ucapan Terima Kasih & Pendahuluan

2. Sifat-sifat universal

3. Produk dalam praktik

4. Sifat-sifat universal dalam geometri aljabar

5. Masalah dengan penggunaan kesetaraan oleh Grothendieck

6. Lebih lanjut tentang pemetaan "kanonik"

7. Isomorfisme kanonik dalam matematika tingkat lanjut

8. Ringkasan Dan Referensi

Ringkasan Dan Referensi

Meskipun saya tidak membuat klaim tentang kesalahan dalam literatur atau celah dalam argumen yang tidak dapat diisi setelah beberapa pekerjaan, saya berpendapat bahwa celah-celah ini memang ada, dan matematika baru mungkin perlu dilakukan oleh para formalis untuk mengisi celah-celah ini dengan cara yang efisien. Celah-celah tersebut terdiri dari dua jenis. Pertama adalah masalah orang-orang yang membuat konstruksi atau membuktikan teorema yang menggunakan secara esensial model objek matematika yang didefinisikan hingga isomorfisme unik; celahnya di sini adalah perlu diperiksa bahwa argumen tersebut tidak bergantung pada detail eksplisit dari model.

\ Para matematikawan sangat menyadari hal ini ketika, misalnya, memilih basis untuk ruang vektor dan kemudian memeriksa bahwa tidak ada hal penting yang bergantung pada pilihan tersebut, atau memilih perwakilan untuk kelas ekuivalensi dan kemudian memeriksa bahwa tidak ada hal penting yang bergantung pada perwakilan tersebut. Namun, mereka tampaknya kurang berhati-hati ketika melakukan matematika yang lebih canggih, membingungkan "sebuah" lokalisasi dengan "lokalisasi tersebut" atau "sebuah" pullback dengan "pullback tersebut", dan menyerahkan kepada pembaca detail pemeriksaan bahwa banyak diagram komutatif.

\ Satu trik yang berguna adalah menyalahgunakan simbol kesetaraan, membuatnya berarti sesuatu yang sebenarnya tidak dimaksudkan; ini dapat menipu pembaca untuk berpikir bahwa tidak ada yang perlu diperiksa. Terkadang pemeriksaan seperti itu bisa sangat menyakitkan, dan mungkin lebih mudah untuk merestrukturisasi argumen matematika daripada benar-benar melakukan pemeriksaan ini. Jenis celah kedua adalah masalah berbagai pemetaan (seperti pemetaan batas dalam urutan eksak) yang dianggap sebagai "kanonik" padahal sebenarnya tidak unik, dan ada pilihan implisit tanda yang dibuat.

\ Sayangnya, tidak sulit sama sekali untuk menunjuk contoh eksplisit dalam literatur di mana penulis tidak menyatakan dengan tepat konvensi mana yang mereka gunakan ketika menyangkut hal-hal seperti teori varietas Shimura, atau aljabar homologis. Ini memberikan beban yang tidak perlu pada matematikawan yang teliti (misalnya Conrad, atau pembuktian teorema komputer) yang mencoba menggunakan atau memverifikasi karya tersebut. Kedua masalah ini telah muncul dalam pekerjaan formalisasi saya, dan saya berharap mereka akan muncul lebih sering saat kita mendalami formalisasi matematika modern.

Referensi

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

:::

:::info Makalah ini tersedia di arxiv di bawah lisensi CC BY 4.0 DEED.

:::

\