दाबी घोषणा गर्नुहोस् । कर्नेलले यो प्रमाणित छ या छैन भन्ने निर्णय गर्दछ ।
मोडेल को एक प्यानल साहित्य संग आफ्नो समस्या आक्रमण, SageMath, PARI/GP र एक एसएमटी Solver, त्यसपछि Mathlib विरुद्ध Lean 4 मा परिणाम formalise. Lean गरेको कर्नेल या त प्रमाण स्वीकार वा यो छैन, र विश्वासी कविता को कुनै पनि मात्रा परिवर्तन कि. जब यो असफल तपाईं शेष कि सटीक लक्ष्य प्राप्त, जो सामान्यतया जहाँ अनौपचारिक तर्क हात-वाफ थियो जहाँ छ।
एउटा जाँचकर्ता जसलाई विश्वास गर्न सकिँदैन
Mathlib प्रकार-चेक अन्तिम कथन Mathlib संग Lean 4, र sorry, native_decide वा ताजा axiom मा leans कि प्रमाण बरु गणना भन्दा अस्वीकार गरिएको छ। यो संगै: SageMath, PARI/GP, Z3, CVC5 र OEIS, त्यसैले एक निर्माण गणना गर्न सकिन्छ र पहिचान कसैले यो बारेमा केही साबित गर्न प्रयास अघि।
असफल प्रमाण फेला परेको छ
जब formalization असफल, लक्ष्य Lean नजिक हुन सक्दैन जुनसुकै सीट यो आक्रमण गर्न सर्वश्रेष्ठ राखिएको हस्तान्तरण छ: बस त्यो लक्ष्य, होइन सम्पूर्ण इतिहास। एक अस्वीकार प्रमाण नाम सटीक, जो सबैभन्दा अनौपचारिक तर्क कहिल्यै भन्दा बढी छ, अन्तराल।
केही पनि दोहोरिएको छैन
प्रत्येक lemma प्यानल स्थापना यसको प्रमाण संग साझेदारी Ledger मा जान्छ, त्यसैले यो कहिल्यै पुन: उत्पन्न र मृत अन्त कहिल्यै retry छन्। लामो समस्याहरू पज र काम गुमाउनु बिना जारी राख्नुहोस्: ट्याब बन्द र भोलि फर्कनुहोस्।