İddianı bildirin. Kernel onun sübut olub olmadığını qərar verəcəkdir.

Modellərin bir paneli sizin probleminizi ədəbiyyat, SageMath, PARI/GP və SMT həlledicisi ilə hücum edir, sonra nəticəni Lean 4 ilə Mathlib arasında formallaşdırır. Lean'ın kerneli ya sübutları qəbul edir ya da qəbul etmir, və heç bir şübhəsiz prosa bu dəyişikliyi dəyişmir. Bacarmadığı zaman qalan doğru məqsədi əldə edirsiniz, bu da adətən qeyri-rəsmi arqumentin əl-ayaq hərəkəti olduğu yerdir.

Məqsəd
done'nin nə demək olduğuna dair konkret ol. 'X'in doğru olub olmadığını qərar ver və onu sübut et' beats 'tell me about X'.
Təmizləmək üçün lazım olan çubuq
Hakim bu barları mətnlə saxlayır. Mükafat səviyyəli bir sübut istəyin və panelin qalibiyyət elan etmək əvəzinə az olduğu zaman sizə açıqca xəbər verəcək.
Panel
Daha çox yer daha çox bucaq və daha çox tur xərcinə səbəb olur.
Hakim
Bu qaydalar əsasında hər bir sübut yenidən yoxlanılır və ən güclü modeliniz dəyərlidir.
Dön
Satınalma limiti
Bu düyməni basmaqla match-i dayandıra bilərsiniz. Heç nə itirmirsiniz.
Görünmə
match-i başlatmaq üçün qeydiyyatdan keçin
Yeni hesablar real match-ə qədər kredit əldə edirlər.
Tə'sirləndirilməyəcək bir yoxlayıcı

Lean 4 ilə Mathlib son ifadəni tip-yoxlayır və sorry, native_decide və ya yeni aksioma ilə bağlı sübut sayılmaq əvəzinə rədd edilir. Onun yanında: SageMath, PARI/GP, Z3, CVC5 və OEIS, belə ki, bir quruluş heç kim onunla bağlı bir şeyi sübut etməyə çalışmadan əvvəl hesablana və müəyyən edilə bilər.

Bacarılmayan sübut tapıntıdır

Formallaşdırma uğursuz olduqda, Lean'ın bağlaya bilmədiyi məqsəd hücum etmək üçün ən yaxşı mövqeyə veriləcəkdir: yalnız bu məqsəd, bütün tarixçə deyil. Təklif edilən sübut boşluğu dəqiq adlandırır, bu da çoxlu qeyri-formal arqumentlərin etdiyindən daha çoxdur.

Heç nə iki dəfə sübut edilmir

Panelin müəyyən etdiyi hər bir lemma öz sübutu ilə paylaşılan bir kitabçaya gedir, buna görə də heç vaxt yenidən əldə edilmir və heç vaxt sonsuzluğa uğramır. Uzun problemlər iş itirilmədən dayandırılır və davam etdirilir: səkməni bağla və sabah geri gəl.