Theorem.chat-ə qədər
Theorem.chat riyazi iddianı qəbul edir və onu həll etməyə çalışır. Siz iddianı və onun cavab verəcəyi standartı bildirirsiniz. İstəydiyiniz qədər AI modellərinin paneli - istədiyiniz satıcıdan - ona hücum edir və bir daha model hakimi. Sonra arqument Lean 4 ilə Mathlib arasında formallaşdırılır və Lean kerneli onun sübut olub olmadığını qərara alır. Sonuncu addım məhsuldur.
Niyə başqa model deyil, kernel
Modelə çətin bir sual ver və doğru olub-olmadığına dair aydın cavab al. Bir neçə sual ver və onlar tez-tez razılaşacaqlar, bu da təsdiq kimi görünsə də, belə deyil: modellər təlim məlumatlarını və kör nöqtələrini paylaşırlar. Birinci modelin ikinci modelini yoxlayan ikinci model eyni növ qərardır və bu barədə ətraflı danışa bilərik. Lean kerneli bunu edə bilməz. Ya axiomlardan və Mathlib-dən ifadəni götürür, ya da etmir və etibar nəticəyə təsir etmir.
Formalı sübutları saxtalaşdırmaq üçün istifadə edilən ənənəvi üsullar yoxlanılaraq rədd edilir. sorry ilə boşluq buraxan, native_decide-ə müraciət edərək kerneli etibarlı hesablama aparmağa vadar edən, ya da yeni aksiom təqdim edən sübutlar aşkar edilir və müvəffəqiyyət hesablanmaq əvəzinə rədd edilir.
Panelin həqiqətən edə biləcəyi şeylər
Mübahisə ucuz hissədir. Panel arXiv, OpenAlex, Crossref kimi kitablarla işləyir - bu səbəbdən də bilinən nəticə pis şəkildə yenidən alınmamaq üçün sitat gətirilir. Hesablama üçün SageMath və PARI/GP, SMT həlli üçün Z3 və CVC5, qurulan ardıcıllığı müəyyən etmək üçün OEIS axtarışı və şəbəkəyə çıxışı olmayan sandbox Python mühiti var. Hesablama heç kəsin onu sübut etməyə çalışmadan əvvəl on minlərlə hallarla test edilə bilər və qarşı nümunə müzakirəni dərhal bitir.
Şəkil
Bir uyğunluq arqument keyfiyyətinə görə qiymətləndirilmir. İddia qəbul şərtlərinə bölünür və şərt yalnız arxasındakı bir şey üçüncü tərəf tərəfindən yenidən yoxlana bildiyi zaman həll edilir: uyğun bir keçidlə mənbə, ya da həqiqətən real çıxıntı ilə yerinə yetirilmiş kod. Hakim qərar verməzdən əvvəl öz sübutlarını yenidən yoxlayır və şərt açıq olduğu müddətdə uyğunluğu bitmiş elan edə bilməz.
Sən sənsən
Standart sizin seçdiyinizdir və hakim onu hərfi mənada saxlayır. Bir diqqətli mütəxəssisin qəbul edəcəyini soruşun və siz onu alacaqsınız. Hər bir ehtimalla tam bir deduktiv arqument istəyin və siz bunun əvəzinə buna qarşı hökm veriləcəksiniz. Mükafat təqdimatının qarşılaşacağı bar üçün soruşun və ədalətli nəticə adətən panelin nə qədər az olduğunun dəqiq hesabatıdır - bu da özünüzə yoxlamağınız lazım olan etibarlı iddiadan daha dəyərlidir.
Bu barədə aydınlıq gətirmək üçün: bu açıq problemləri həll edən maşın deyil. Bu, həll olunmamış arqumentin həll edilmiş kimi keçməsinə icazə verməyəcək və sizə hansı addımda səhv olduğunu tam olaraq bildirəcək maşındır.
Bacarılmayan formalizasiya faydalı çıxıntıdır
Lean sübutları bağlamadığı zaman, qalan hədəfi əldə edirsiniz. Əsas olaraq bu, formal arqumentin əl-ayaq hərəkəti etdiyi yerdir - hər kəsin prosa versiyasını oxuduğunu və keçdiyi addımdır. Bu hədəf sonradan hücum etmək üçün ən yaxşı yer olan yerə, artıq sınanmış şeylərlə birlikdə və başqa heç nə ilə birlikdə verilir. Modellər tıxandıqda, özlərini tam qiymətə yenidən ifadə edərək, yıxılırlar; əvəzində bir spesifik sual vermək, adətən, tokenlərin bir hissəsi üçün bloku açır.
Uzun iş davam edir
Panelin müəyyən etdiyi hər bir lemma öz sübutu ilə paylaşılan bir kitabçaya daxil olur, nəticələr bir dəfə yazılaraq heç vaxt yenidən əldə edilməz, və heç kim geri qayıtmaz deyə sonsuzluqlar qeyd edilir. Müvafiqliklər server tərəfində işləyir və təmiz dayanır - büdcədə, provayderin işləməməsi zamanı, ya da səkinə bağladığınız üçün - və dayandıqları yerdə davam edir.
Bu nədir
Teorem deduktiv sözdür. Bu sayt riyaziyyat, məntiq, nəzəri kompüter elmləri, nəzəri fizika və iqtisadi nəzəriyyə üçün yaradılmışdır - iddianın sübutla həll olunduğu sahələr. Biologiya, tibb, kimya və sosial elmlərdə empirik suallar teoremlər deyil, tapıntılar yaradır və heç bir formalizasiya onları həll edə bilməz. Bizim bacı saytımız referee.chat də eyni panel-and-referee prosesini Lean addımsız, elə bu suallar üçün işlədir.