İ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

Careful expert

What a competent professional in the field would accept as done and correct.

Publication standard

Would survive peer review: every claim sourced or derived, methods stated, limitations acknowle…

Formal proof

A complete deductive argument. Every step justified, every assumption stated, no appeals to pla…

Prize standard

The bar a Clay Millennium Prize submission would face: a complete, self-contained, gap-free pro…

Decision-grade

Enough evidence to act on commercially: options costed, risks named, recommendation justified.

Write my own

Describe your own standard.

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 oyun dayandırılır. Heç nə itirmirsiniz.

Görünmə

_Başlandığı zaman yayımla

Bir oyun başlatmaq üçün qeyd olun

Yeni hesablar real matç üçün kifayət 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.