আনুষ্ঠানিক প্রমাণ সিস্টেমগুলি উন্নত গণিতে উপেক্ষিত অস্পষ্টতা প্রকাশ করে

লিঙ্কের তালিকা

সারসংক্ষেপ

1. স্বীকৃতি ও ভূমিকা

২. সার্বজনীন বৈশিষ্ট্য

৩. বাস্তবে গুণফল

৪. বীজগাণিতিক জ্যামিতিতে সার্বজনীন বৈশিষ্ট্য

৫. গ্রোথেনডিকের সমতা ব্যবহারের সমস্যা

৬. "ক্যানোনিকাল" মানচিত্র সম্পর্কে আরও

৭. উন্নত গণিতে ক্যানোনিকাল আইসোমরফিজম

৮. সারাংশ এবং তথ্যসূত্র

সারাংশ এবং তথ্যসূত্র

যদিও আমি সাহিত্যে ত্রুটি বা যুক্তিতে ফাঁক সম্পর্কে কোন দাবি করছি না যা কিছু কাজের পরে পূরণ করা যায় না, আমি যুক্তি দিচ্ছি যে এই ফাঁকগুলি বিদ্যমান, এবং এই ফাঁকগুলি দক্ষভাবে পূরণ করার জন্য আনুষ্ঠানিকতাকারীদের দ্বারা নতুন গণিত করা প্রয়োজন হতে পারে। ফাঁকগুলি দুই ধরনের। প্রথমত, মানুষ যখন এমন নির্মাণ করে বা উপপাদ্য প্রমাণ করে যা একটি গাণিতিক বস্তুর মডেলের অপরিহার্য ব্যবহার করে যা অনন্য আইসোমরফিজম পর্যন্ত সংজ্ঞায়িত করা হয়; এখানে ফাঁকটি হল এটি যাচাই করা প্রয়োজন যে যুক্তিটি মডেলের স্পষ্ট বিবরণের উপর নির্ভর করে না।

\ গণিতবিদরা এই বিষয়ে ভালভাবে অবগত যখন, উদাহরণস্বরূপ, একটি ভেক্টর স্পেসের জন্য একটি ভিত্তি নির্বাচন করা এবং তারপর যাচাই করা যে কোন গুরুত্বপূর্ণ বিষয় পছন্দের উপর নির্ভর করে না, বা একটি সমতুল্য শ্রেণীর জন্য একটি প্রতিনিধি নির্বাচন করা এবং তারপর যাচাই করা যে কোন গুরুত্বপূর্ণ বিষয় প্রতিনিধির উপর নির্ভর করে না। যাইহোক, তারা আরও উন্নত গণিত করার সময় কম সতর্ক বলে মনে হয়, "একটি" লোকালাইজেশন কে "দি" লোকালাইজেশন এর সাথে বিভ্রান্ত করে বা "একটি" পুলব্যাক কে "দি" পুলব্যাক এর সাথে বিভ্রান্ত করে, এবং পাঠকের জন্য অনেক ডায়াগ্রাম কমিউট করে কিনা তা যাচাই করার বিবরণ ছেড়ে দেয়।

\ একটি উপযোগী কৌশল হল সমতা প্রতীকের অপব্যবহার করা, এটিকে এমন কিছু অর্থ দেওয়া যা এর অর্থ নয়; এটি পাঠককে এই ভাবনায় প্রতারিত করতে পারে যে কিছুই যাচাই করার প্রয়োজন নেই। কখনও কখনও এই ধরনের যাচাইগুলি আশ্চর্যজনকভাবে কষ্টকর হতে পারে, এবং এই যাচাইগুলি প্রকৃতপক্ষে করার চেয়ে একটি গাণিতিক যুক্তি পুনর্গঠন করা সহজ হতে পারে। দ্বিতীয় ধরনের ফাঁক হল বিভিন্ন মানচিত্রের সমস্যা (যেমন সঠিক ক্রমে সীমানা মানচিত্র) যা "ক্যানোনিকাল" হিসাবে বিবেচিত হয় যেখানে এখন তারা প্রকৃতপক্ষে অনন্য নয়, এবং চিহ্নের অন্তর্নিহিত পছন্দ করা হচ্ছে।

\ দুর্ভাগ্যবশত, সাহিত্যে স্পষ্ট উদাহরণ দেখানো মোটেও কঠিন নয় যেখানে একজন লেখক শিমুরা বৈচিত্র্যের তত্ত্ব বা হোমোলজিকাল বীজগণিতের মতো বিষয়ে আসলে তারা কোন কনভেনশন ব্যবহার করছেন তা সঠিকভাবে উল্লেখ করেন না। এটি সতর্ক গণিতবিদের (উদাহরণস্বরূপ কনরাড, বা একটি কম্পিউটার থিওরেম প্রুভার) উপর অপ্রয়োজনীয় বোঝা চাপায় যিনি কাজটি ব্যবহার বা যাচাই করার চেষ্টা করছেন। এই উভয় সমস্যা আমার আনুষ্ঠানিকীকরণ কাজে দেখা গেছে, এবং আমি আশা করি যে আমরা আধুনিক গণিতের আনুষ্ঠানিকীকরণে আরও গভীরে যাওয়ার সাথে সাথে এগুলি আরও প্রায়শই দেখা যাবে।

তথ্যসূত্র

[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 লাইসেন্সের অধীনে।

:::

\