দাবিটি উল্লেখ করুন। কার্নেল সিদ্ধান্ত নেয় এটি প্রমাণিত কিনা।

মডেলের একটি প্যানেল আপনার সমস্যাকে সাহিত্য, SageMath, PARI/GP এবং একটি SMT সমাধানকারীর সাথে আক্রমণ করে, তারপর Lean 4 এর বিরুদ্ধে Mathlib এর ফলাফলকে সরকারি করে। লিনের কার্নেল প্রমাণ গ্রহণ করে অথবা না করে, এবং কোন পরিমাণ নিশ্চিত প্রবন্ধের পরিবর্তন করে না। যখন এটি ব্যর্থ হয় তখন আপনি সঠিক লক্ষ্য পাবেন যা অবশিষ্ট আছে, যা সাধারণত অপ্রকাশিত যুক্তি ছিল হাত- উঁচু করে।

লক্ষ্য
done মানে কি তা স্পষ্ট করে বলুন। 'X সত্য কি না তা নির্ধারণ করুন এবং প্রমাণ করুন' 'X সম্পর্কে আমাকে বলুন'-কে টপকে যায়।
বারটিকে পরিষ্কার করতে হবে
রেফারি এই বার্ডটি আক্ষরিক অর্থে ধরে রাখেন। পুরস্কার স্তরের প্রমাণ চাইলে তা আপনাকে স্পষ্টভাবে বলবে যখন প্যানেলের সংখ্যা কম হবে, বিজয় ঘোষণা করার পরিবর্তে।
প্যানেল
আরো আসন মানে আরো কোণ, আর প্রতি রাউন্ডে আরো খরচ।
রেফারি
নীতিমালা অনুযায়ী নিয়ম আর প্রত্যেকটা প্রমাণের পুনঃপরীক্ষা, তোমার সবচেয়ে শক্তিশালী মডেলকে মূল্যবান করে তোলে।
রান
ব্যয় সীমা
Hitting it pauses the match. Nothing is lost.
দৃশ্যমানতা
match শুরু করতে সাইন আপ করুন
New accounts get starting credit, enough for a real match.
একটি চেকার যাকে রাজি করা যায় না

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

ব্যর্থ প্রমাণ একটি খুঁজে পেতে

যখন সরকারি ভাবে যুক্তি প্রদান ব্যর্থ হয়, তখন যে লক্ষ্য লেন পেরিয়ে যেতে পারেননি, সেটিকে আক্রমণ করার জন্য যে কোন স্থানে সেটিকে তুলে দেয়া হয়: শুধুমাত্র সেই লক্ষ্য, পুরো ইতিহাস নয়।

কিছুই দুইবার প্রমাণিত হয় না

প্রতিটি lemma প্যানেল প্রতিষ্ঠা একটি শেয়ার করা লেজার তার প্রমাণ সঙ্গে যায়, তাই এটি কখনোই পুনরায় উদ্ভূত এবং dead ends কখনোই পুনরায় চেষ্টা করা হয় না । দীর্ঘ সমস্যা স্থগিত এবং কাজ হারানো ছাড়া পুনরায় শুরু: ট্যাব বন্ধ এবং আগামীকাল ফিরে আসো ।