350 साल पुराने कठिन प्रश्न 'Fermat's Last Theorem' के कंप्यूटर-आधारित प्रमाण पर जुटे गणितज्ञ

Fermat's Last Theorem को कंप्यूटर भाषा में फिर से सिद्ध किया जाएगा

• Imperial College London के प्रोफेसर Kevin Buzzard अक्टूबर 2024 से Fermat's Last Theorem (FLT) का formal proof Lean theorem prover में लिखने वाले हैं.
• ब्रिटेन की [Engineering and Physical Sciences Research Council EPSRC]EPSRC ने प्रोफेसर Buzzard को उसी महीने से 5 साल तक इस काम के लिए research funding देने का निर्णय लिया है.
• Lean blueprints नाम के plasTeX plugin का उपयोग कर बनाई गई project plan अप्रैल 2024 के अंत में सार्वजनिक की जाएगी.

क्या Fermat's Last Theorem पहले से सिद्ध नहीं हो चुका?

हाँ, हो चुका है. ब्रिटिश गणितज्ञ Andrew Wiles ने 1994 में इसका प्रमाण प्रस्तुत किया था, और यह प्रमाण 1995 में औपचारिक रूप से प्रकाशित हुआ था. लेकिन [interactive theorem prover ITP]itp की भाषा में लिखा गया formal proof अभी तक मौजूद नहीं है.

Interactive theorem prover? Formal proof? यह क्या है?

• [interactive theorem prover ITP]itp: ऐसा कंप्यूटर प्रोग्राम जो इंसानों को formal proof लिखने में मदद करता है. इसे proof assistant भी कहा जाता है.
• formal proof: ऐसा प्रमाण जिसे proof verifier नामक कंप्यूटर प्रोग्राम से जाँचा जा सके. proof assistant आम तौर पर proof verifier का काम भी करते हैं.

क्या theorem prover artificial intelligence है?

[neural theorem prover NTP]ntp को उस श्रेणी में रखा जा सकता है, लेकिन Lean सहित कई interactive theorem prover machine learning आधारित प्रोग्राम नहीं हैं.

Lean theorem prover का परिचय दीजिए.

• यह interactive theorem prover भी है और pure functional programming language भी.
• यह dependent type theory पर आधारित है.
• इसमें type class, extensible syntax, macro, metaprogramming जैसी सुविधाएँ हैं.
• अन्य proof assistant की तुलना में Lean के user base में ऐसे गणितज्ञ खास तौर पर अधिक हैं जो गणित की बुनियाद से बाहर के क्षेत्रों पर काम करते हैं.

Fermat's Last Theorem का formal proof क्यों लिखा जा रहा है?

प्रोफेसर Kevin Buzzard की X पर की गई post को उद्धृत करें तो, "कंप्यूटर को आधुनिक number theory समझाना है, ताकि अंततः वह number theorists की मदद कर सके."

लिंक

• 3 अक्टूबर 2023 को प्रोफेसर Kevin Buzzard द्वारा Lean Zulip chat में पोस्ट किया गया संदेश: https://leanprover.zulipchat.com/#narrow/stream/113486-announce/topic/…
• Lean mathematics library: https://github.com/leanprover-community/mathlib4
• New Scientist लेख: https://institutions.newscientist.com/article/…
• Popular Mechanics लेख: https://popularmechanics.com/science/math/…

[calofmijuck]

समर्थन करता हूँ। जिन लोगों की Formal proof में रुचि है, उनके लिए प्रोफेसर Terrence Tao की Machine Assisted Proofs (https://www.youtube.com/watch?v=AayZuuDDKP0) व्याख्यान सुनना भी मैं recommend करूँगा।