أنظمة البرهان الرسمية تكشف عن غموض مُغفل في الرياضيات المتقدمة

جدول الروابط

ملخص

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

:::info المؤلف: كيفن بوزارد

:::

:::info هذه الورقة متاحة على arxiv تحت ترخيص CC BY 4.0 DEED.

:::

\