দাবী উল্লেখ কৰক। কাৰনেলে সিদ্ধান্ত ল'ব যে ই প্ৰমাণিত হৈছে নে নাই।
মডেলৰ এটা পেনেলে সাহিত্য, SageMath, PARI/GP আৰু এটা SMT সমাধানকাৰীৰ সৈতে আপোনাৰ সমস্যা আক্ৰমণ কৰে, তাৰ পিছত Lean 4 ত Mathlib ৰ বিৰুদ্ধে ফলাফলৰ আনুষ্ঠানিক কৰে। Lean ৰ কাৰনেলে প্ৰমাণ গ্ৰহণ কৰে অথবা নকৰে, আৰু কোনো পৰিমাণৰ বিশ্বাসযোগ্য প্ৰবন্ধে সেইটো পৰিবৰ্তন নকৰে। যেতিয়া ই ব্যৰ্থ হয় আপুনি সঠিক লক্ষ্য পোৱা যায় যি নাথাকে, যি সাধাৰণতে অপ্ৰচলিত যুক্তি হ'ল হাত-ভৰাই থকা।
এটা চেকাৰ যিক অনুপ্ৰেৰণা কৰিব নোৱাৰি
Lean 4 ৰ সৈতে Mathlib ৰ ধৰণ-পৰীক্ষণে অন্তিম বিবৃতি পৰীক্ষা কৰে, আৰু এটা প্ৰমাণ যি sorry, native_decide অথবা এটা নতুন স্বতন্ত্ৰত নির্ভরশীল সেইটো গণনা কৰাৰ পৰিবৰ্তে নাকচ কৰা হয়। ইয়াৰ পাশে: SageMath, PARI/GP, Z3, CVC5 আৰু OEIS, গতিকে এটা গঠনক গণনা কৰা আৰু চিনাক্ত কৰা যাব যিকোনো এটাৰ বিষয়ে একো প্ৰমাণ কৰাৰ চেষ্টা কৰাৰ পূৰ্বে।
এটা ব্যৰ্থ প্ৰমাণ এটা সন্ধান
যেতিয়া আনুষ্ঠানিকীকৰণ ব্যৰ্থ হয়, লক্ষ্য Lean বন্ধ কৰিব নোৱাৰিলে যিকোনো স্থানত আক্ৰমণ কৰিবলৈ সৰ্বোত্তম স্থানত স্থানান্তৰ কৰা হয়: কেৱল সেই লক্ষ্য, সম্পূৰ্ণ ইতিহাস নহয়। এটা নাকচ কৰা প্ৰমাণে গভীৰতা সঠিকভাৱে নামকৰণ কৰে, যি অধিকাংশ অপ্ৰচলিত যুক্তিৰ পৰা অধিক।
কোনো কথা দুবাৰ প্ৰমাণিত নহয়
পেনেল দ্বাৰা প্ৰতিষ্ঠিত প্ৰতিটো লেমা এটা অংশীদাৰী লেজাৰত তাৰ প্ৰমাণৰ সৈতে যায়, গতিকে ইয়াক কেতিয়াও পুনৰ-উৎপাদন কৰা নহয় আৰু বন্ধ সমাপ্তিসমূহ কখনোই পুনৰ চেষ্টা কৰা নহয়। দীৰ্ঘ সমস্যাসমূহ কাম হেৰুৱাব নোহোৱাকৈ স্থগিত আৰু পুনৰাবৃত্তি কৰক: টেব বন্ধ কৰক আৰু কাইলৈ পুনৰ আহিব।