سیستم‌های اثبات رسمی، ابهامات نادیده گرفته شده در ریاضیات پیشرفته را آشکار می‌کنند

جدول پیوندها

چکیده

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 نویسنده: کوین بازارد

:::

:::info این مقاله در arxiv تحت مجوز CC BY 4.0 DEED در دسترس است.

:::

\