দাবী উল্লেখ কৰক। কাৰনেলে সিদ্ধান্ত ল'ব যে ই প্ৰমাণিত হৈছে নে নাই।

Lean 4 ৰ সৈতে Mathlib ৰ ধৰণ-পৰীক্ষণে অন্তিম বিবৃতি পৰীক্ষা কৰে, আৰু এটা প্ৰমাণ যি sorry, native_decide অথবা এটা নতুন স্বতন্ত্ৰত নির্ভরশীল সেইটো গণনা কৰাৰ পৰিবৰ্তে নাকচ কৰা হয়। ইয়াৰ পাশে: SageMath, PARI/GP, Z3, CVC5 আৰু OEIS, গতিকে এটা গঠনক গণনা কৰা আৰু চিনাক্ত কৰা যাব যিকোনো এটাৰ বিষয়ে একো প্ৰমাণ কৰাৰ চেষ্টা কৰাৰ পূৰ্বে।

যেতিয়া আনুষ্ঠানিকীকৰণ ব্যৰ্থ হয়, লক্ষ্য Lean বন্ধ কৰিব নোৱাৰিলে যিকোনো স্থানত আক্ৰমণ কৰিবলৈ সৰ্বোত্তম স্থানত স্থানান্তৰ কৰা হয়: কেৱল সেই লক্ষ্য, সম্পূৰ্ণ ইতিহাস নহয়। এটা নাকচ কৰা প্ৰমাণে গভীৰতা সঠিকভাৱে নামকৰণ কৰে, যি অধিকাংশ অপ্ৰচলিত যুক্তিৰ পৰা অধিক।

পেনেল দ্বাৰা প্ৰতিষ্ঠিত প্ৰতিটো লেমা এটা অংশীদাৰী লেজাৰত তাৰ প্ৰমাণৰ সৈতে যায়, গতিকে ইয়াক কেতিয়াও পুনৰ-উৎপাদন কৰা নহয় আৰু বন্ধ সমাপ্তিসমূহ কখনোই পুনৰ চেষ্টা কৰা নহয়। দীৰ্ঘ সমস্যাসমূহ কাম হেৰুৱাব নোহোৱাকৈ স্থগিত আৰু পুনৰাবৃত্তি কৰক: টেব বন্ধ কৰক আৰু কাইলৈ পুনৰ আহিব।