लीन 4 में फ़र्मेट के अंतिम प्रमेय का एक पूर्ण, मशीन-जाँचित प्रमाण, जो Mathlib (लीन 4.33.1; Mathlib v4.33.0) पर निर्मित है। तर्क Frey, Serre, Ribet, Wiles और Taylor-Wiles का अनुसरण करता है। रिपॉजिटरी में PROOF-PATH.md और ब्राउज़िंग के लिए एक html फ़ोल्डर शामिल है।

यह शोध आर्टिफैक्ट अनुरक्षित नहीं है और योगदान स्वीकार नहीं करता है। प्रमेय कहता है कि प्राकृतिक संख्याओं n ≥ 3 और धनात्मक a, b, c के लिए, a^n + b^n ≠ c^n। बिल्ड सत्यापित करता है कि प्रमाण केवल लीन के तीन मानक अभिगृहीतों पर निर्भर करता है, बिना किसी sorry या अतिरिक्त अभिगृहीतों के।

सत्यापन में एक नए सिरे से lake बिल्ड, चुनौती के विरुद्ध एक तुलनित्र जाँच, और एक स्वतंत्र Rust कर्नेल (nanoda) शामिल था जिसने 1,052,234 घोषणाओं की जाँच की। तुलनित्र ने पुष्टि की कि कथन चुनौती से मेल खाता है और केवल Mathlib का उपयोग करता है।

html फ़ोल्डर (लगभग 390 MB) प्रमाण को स्थिर वेब पृष्ठों के रूप में प्रस्तुत करता है, जिसमें 29,511 प्रमेय और 1,450 परिभाषा मॉड्यूल हैं, जो ऑफ़लाइन खोजने और ब्राउज़ करने योग्य हैं।

प्रमुख संस्थाएँ: कंपनियाँ: GitHub | लोग: Frey, Serre, Ribet, Wiles, Taylor-Wiles

सामान्य प्रश्न: लीन 4 में फ़र्मेट के अंतिम प्रमेय के प्रमाण में क्या शामिल है?

लीन 4 में प्रमाण Frey, Serre, Ribet, Wiles और Taylor-Wiles के तर्क को औपचारिक रूप देता है। यह Mathlib पर निर्मित है और लीन कर्नेल, एक तुलनित्र और एक स्वतंत्र Rust कर्नेल द्वारा सत्यापित है। प्रमाण केवल लीन के मानक अभिगृहीतों का उपयोग करता है और कोई अतिरिक्त धारणा नहीं।