ระบบการพิสูจน์อย่างเป็นทางการเปิดเผยความคลุมเครือที่มองข้ามในคณิตศาสตร์ขั้นสูง

ตารางลิงก์

บทคัดย่อ

1. กิตติกรรมประกาศและบทนำ

2. คุณสมบัติสากล

3. ผลิตภัณฑ์ในทางปฏิบัติ

4. คุณสมบัติสากลในเรขาคณิตพีชคณิต

5. ปัญหาเกี่ยวกับการใช้ความเท่ากันของ Grothendieck

6. เพิ่มเติมเกี่ยวกับแผนที่ "มาตรฐาน"

7. ไอโซมอร์ฟิซึมมาตรฐานในคณิตศาสตร์ขั้นสูง

8. สรุปและเอกสารอ้างอิง

สรุปและเอกสารอ้างอิง

แม้ว่าผมไม่ได้กล่าวอ้างถึงข้อผิดพลาดในวรรณกรรมหรือช่องว่างในข้อโต้แย้งที่ไม่สามารถเติมเต็มได้หลังจากทำงานบางอย่าง แต่ผมกำลังโต้แย้งว่าช่องว่างเหล่านี้มีอยู่จริง และอาจจำเป็นต้องมีคณิตศาสตร์ใหม่ที่ต้องทำโดยผู้ทำให้เป็นทางการเพื่อเติมเต็มช่องว่างเหล่านี้อย่างมีประสิทธิภาพ ช่องว่างมีสองประเภท ประการแรกคือปัญหาที่คนสร้างโครงสร้างหรือพิสูจน์ทฤษฎีบทที่ใช้แบบจำลองของวัตถุทางคณิตศาสตร์ซึ่งถูกกำหนดขึ้นจนถึงไอโซมอร์ฟิซึมที่ไม่ซ้ำกัน ช่องว่างตรงนี้คือต้องตรวจสอบว่าข้อโต้แย้งไม่ได้ขึ้นอยู่กับรายละเอียดที่ชัดเจนของแบบจำลอง

\ นักคณิตศาสตร์ตระหนักดีเกี่ยวกับเรื่องนี้เมื่อพูดถึงการเลือกฐานสำหรับปริภูมิเวกเตอร์แล้วตรวจสอบว่าไม่มีสิ่งสำคัญใดขึ้นอยู่กับตัวเลือก หรือการเลือกตัวแทนสำหรับคลาสสมมูลแล้วตรวจสอบว่าไม่มีสิ่งสำคัญใดขึ้นอยู่กับตัวแทน อย่างไรก็ตาม พวกเขาดูเหมือนจะระมัดระวังน้อยลงเมื่อทำคณิตศาสตร์ขั้นสูง สับสนระหว่าง "การทำให้เป็นท้องถิ่น" กับ "การทำให้เป็นท้องถิ่น" หรือ "การดึงกลับ" กับ "การดึงกลับ" และปล่อยให้ผู้อ่านตรวจสอบรายละเอียดว่าแผนภาพหลายแผนภาพสอดคล้องกัน

\ เทคนิคที่มีประโยชน์อย่างหนึ่งคือการใช้สัญลักษณ์ความเท่ากันในทางที่ผิด ทำให้มันหมายถึงบางสิ่งที่มันไม่ได้หมายถึง นี่สามารถหลอกผู้อ่านให้คิดว่าไม่จำเป็นต้องตรวจสอบอะไร บางครั้งการตรวจสอบดังกล่าวอาจเจ็บปวดอย่างน่าประหลาดใจ และอาจง่ายกว่าที่จะปรับโครงสร้างข้อโต้แย้งทางคณิตศาสตร์มากกว่าที่จะทำการตรวจสอบเหล่านี้จริงๆ ช่องว่างประเภทที่สองคือปัญหาของแผนที่ต่างๆ (เช่น แผนที่ขอบในลำดับที่แน่นอน) ที่ถูกมองว่าเป็น "มาตรฐาน" ซึ่งในความเป็นจริงแล้วไม่ได้มีเอกลักษณ์ และมีการเลือกเครื่องหมายโดยนัยที่กำลังเกิดขึ้น

\ น่าเสียดายที่ไม่ยากเลยที่จะชี้ไปที่ตัวอย่างที่ชัดเจนในวรรณกรรมที่ผู้เขียนไม่ได้ระบุอย่างแน่ชัดว่ากำลังใช้ข้อตกลงใดเมื่อพูดถึงสิ่งต่างๆ เช่น ทฤษฎีของ Shimura varieties หรือพีชคณิตโฮโมโลจิคัล สิ่งนี้สร้างภาระที่ไม่จำเป็นให้กับนักคณิตศาสตร์ที่รอบคอบ (เช่น Conrad หรือโปรแกรมพิสูจน์ทฤษฎีบทคอมพิวเตอร์) ที่กำลังพยายามใช้หรือตรวจสอบงาน ปัญหาทั้งสองนี้ปรากฏในงานการทำให้เป็นทางการของผม และผมคาดว่าจะพบบ่อยขึ้นเมื่อเราลงลึกในการทำให้คณิตศาสตร์สมัยใหม่เป็นทางการมากขึ้น

เอกสารอ้างอิง

[AX23] David Kurniadi Angdinata และ Junyan Xu, การพิสูจน์อย่างเป็นทางการขั้นพื้นฐานของกฎกลุ่มบนเส้นโค้งวงรีไวเออร์สตราสในทุกลักษณะ, การประชุมนานาชาติครั้งที่ 14 เรื่องการพิสูจน์ทฤษฎีบทแบบโต้ตอบ (ITP 2023) (Dagstuhl, เยอรมนี) (Adam Naumowicz และ René Thiemann, eds.), Leibniz International Proceedings in Informatics (LIPIcs), vol. 268, Schloss Dagstuhl – Leibniz-Zentrum für Informatik, 2023, หน้า 6:1– 6:19.

[BCM20] Kevin Buzzard, Johan Commelin, และ Patrick Massot, การทำให้ปริภูมิเพอร์เฟคทอยด์เป็นทางการ, รายงานการประชุมการประชุมนานาชาติ ACM SIGPLAN ครั้งที่ 9 เรื่องโปรแกรมที่ได้รับการรับรองและการพิสูจน์, CPP 2020, นิวออร์ลีนส์, LA, USA, 20-21 มกราคม 2020 (Jasmin Blanchette และ Catalin Hritcu, eds.), ACM, 2020, หน้า 299–312.

[BPL21] Anthony Bordg, Lawrence Paulson, และ Wenda Li, แผนการของ Grothendieck ในเรขาคณิตพีชคณิต, มีนาคม 2021, https://isa-afp.org/entries/Grothendieck_Schemes.html, การพัฒนาการพิสูจน์อย่างเป็นทางการ.

[Buz] Kevin M. Buzzard, แนวทางของ Grothendieck ต่อความเท่ากัน, https://www.youtube.com/watch?v=-OjCMsqZ9ww, เข้าถึงเมื่อ: 12-08-2023. [Buz19] Buzzard, Kevin, ส่วนกลับของการเป็นไบเจคชัน, 2019, [ออนไลน์; เข้าถึงเมื่อ 12-Aug-2023].

[Con00] Brian Conrad, ความสมมาตรของ Grothendieck และการเปลี่ยนฐาน, Lecture Notes in Mathematics, vol. 1750, Springer-Verlag, Berlin, 2000. MR 1804902

[dFF23] María Inés de Frutos-Fernández, การทำให้การขยายบรรทัดฐานและการประยุกต์ใช้กับทฤษฎีจำนวนเป็นทางการ, การประชุมนานาชาติครั้งที่ 14 เรื่องการพิสูจน์ทฤษฎีบทแบบโต้ตอบ (ITP 2023) (Dagstuhl, เยอรมนี) (Adam Naumowicz และ René Thiemann, eds.), Leibniz International Proceedings in Informatics (LIPIcs), vol. 268, Schloss Dagstuhl – LeibnizZentrum für Informatik, 2023, หน้า 13:1–13:18.

[Gro60] A. Grothendieck, องค์ประกอบของเรขาคณิตพีชคณิต. I. ภาษาของแผนการ, Inst. Hautes Etudes Sci. Publ. Math. (1960), no. 4, 228. MR 217083

[Lan97] R. P. Langlands, การแทนของกลุ่มพีชคณิตอาบีเลียน, Pacific J. Math. (1997), 231–250, Olga Taussky-Todd: in memoriam. MR 1610871

[Liv23] Amelia Livingston, โคโฮโมโลจีกลุ่มในห้องสมุดชุมชน Lean, การประชุมนานาชาติครั้งที่ 14 เรื่องการพิสูจน์ทฤษฎีบทแบบโต้ตอบ (ITP 2023) (Dagstuhl, เยอรมนี) (Adam Naumowicz และ René Thiemann, eds.), Leibniz International Proceedings in Informatics (LIPIcs), vol. 268, Schloss Dagstuhl – Leibniz-Zentrum für Informatik, 2023, หน้า 22:1–22:17.

[mC20] ชุมชน mathlib, ห้องสมุดคณิตศาสตร์ lean, รายงานการประชุมการประชุมนานาชาติ ACM SIGPLAN ครั้งที่ 9 เรื่องโปรแกรมที่ได้รับการรับรองและการพิสูจน์, ACM, มกราคม 2020.

[Mil80] James S. Milne, โคโฮโมโลจีอีทาล, Princeton Mathematical Series, No. 33, Princeton University Press, Princeton, N.J., 1980. MR 559531

[Sta18] ผู้เขียนโครงการ Stacks, โครงการ Stacks, https://stacks.math.columbia.edu, 2018.

[Wei59] André Weil, จดหมายโต้ตอบ [ลงนามโดย "R. Lipschitz"], Ann. of Math. (2) 69 (1959), 247–251, ยกให้กับ A. Weil. MR 100637 [Wik04a] ผู้มีส่วนร่วมใน Wikipedia, หมวดหมู่โมนอยดัล — Wikipedia, สารานุกรมเสรี, 2004, [ออนไลน์; เข้าถึงเมื่อ 12-Aug-2023].

[Wik04b] , คู่อันดับ — Wikipedia, สารานุกรมเสรี, 2004, [ออนไลน์; เข้าถึงเมื่อ 20-May-2023].

[Zha23] Jujian Zhang, การทำให้การสร้าง Proj ใน Lean เป็นทางการ, การประชุมนานาชาติครั้งที่ 14 เรื่องการพิสูจน์ทฤษฎีบทแบบโต้ตอบ (ITP 2023) (Dagstuhl, เยอรมนี) (Adam Naumowicz และ René Thiemann, eds.), Leibniz International Proceedings in Informatics (LIPIcs), vol. 268, Schloss Dagstuhl – Leibniz-Zentrum für Informatik, 2023, หน้า 35:1– 35:17.

[ZM23] Max Zeuner และ Anders Mörtberg, การทำให้แผนการแอฟฟีนเชิงสร้างเป็นทางการแบบยูนิวาเลนท์, 2023. อีเมล: [e-mail] ภาควิชาคณิตศาสตร์, Imperial College London

:::info ผู้เขียน: KEVIN BUZZARD

:::

:::info บทความนี้มีอยู่บน arxiv ภายใต้ใบอนุญาต CC BY 4.0 DEED

:::

\