દાવો સ્પષ્ટ કરો. કર્નલ નક્કી કરે છે કે શું તે સાબિત થયેલ છે.

મોડેલોની પેનલ તમારી સમસ્યા પર લખાણ, SageMath, PARI/GP અને SMT ઉકેલક સાથે હુમલો કરે છે, પછી Lean 4 માં Mathlib વિરુદ્ધ પરિણામને ઔપચારિક બનાવે છે. લીનની કર્નલ અથવા તો સાબિત કરે છે કે તે નથી કરતું, અને વિશ્વાસપાત્ર પ્રસ્તુતિની કોઈ માત્રા તે બદલતી નથી. જ્યારે તે નિષ્ફળ જાય છે ત્યારે તમે ચોક્કસ લક્ષ્ય મેળવો છો જે બાકી રહે છે, જે સામાન્ય રીતે અનિશ્ચિત દલીલ હાથ-વગાડતી હતી.

લક્ષ્ય
શું થયું તે વિશે સ્પષ્ટ રહો. 'કહી દો કે X સાચું છે, અને તે સાબિત કરો કે' 'મને X વિશે કહો' બરાબર છે.
પટ્ટી કે જેને સાફ કરવી પડશે
રેફરી આ પટ્ટી વાસ્તવિક રીતે ધરાવે છે. પુરસ્કાર-સ્તરનાં પુરાવા માટે પૂછો અને તે તમને સ્પષ્ટપણે કહેશે કે જ્યારે પેનલ ટૂંકી પડે છે, જીતની જાહેરાત કરવાને બદલે.
પેનલ
વધુ બેઠકોનો અર્થ વધુ ખૂણા અને રાઉન્ડ દીઠ વધુ ખર્ચ થાય છે.
રેફરી
માપદંડ પર નિયમો અને પુરાવાનું દરેક પાસું ફરીથી ચકાસે છે. તમારું સૌથી મજબૂત મોડેલ.
રાઉન્ડ્સ
ખર્ચ મર્યાદા
તેને ઠોકવાથી match અટકાવે છે. કંઇક ગુમ થયેલ છે.
દૃશ્યમાનતા
match શરૂ કરવા માટે નોંધણી કરો
નવા ખાતાઓ શરૂઆતના ક્રેડિટ સાથે શરૂ થાય છે, જે ખરેખર match માટે પૂરતું છે.
ચકાસનાર કે જેને સમજાવી શકાતુ નથી

Mathlib સાથે Lean 4 પ્રકાર-ચકાસણી અંતિમ વાક્ય છે, અને સાબિત કરે છે કે જે sorry, native_decide અથવા તાજા અક્ષય પર લઇ જાય છે તે ગણતરી કરતા નકારવામાં આવે છે. તેની સાથે: SageMath, PARI/GP, Z3, CVC5 અને OEIS, તેથી કોઈપણ તે વિશે કંઇક સાબિત કરવાનો પ્રયત્ન કરે તે પહેલાં નિર્માણ ગણવામાં આવે છે અને ઓળખવામાં આવે છે.

નિષ્ફળ સાબિત કરનાર શોધ છે

જ્યારે ઔપચારિકીકરણ નિષ્ફળ જાય છે, ત્યારે લક્ષ્ય Lean close કરી શકતું નથી તે તેને હુમલો કરવા માટે શ્રેષ્ઠ સ્થાને મૂકવામાં આવે છે: માત્ર તે લક્ષ્ય, સંપૂર્ણ ઇતિહાસ નથી. અસ્વીકાર્ય સાબિત કરનાર ખાલી જગ્યાનું નામ ચોક્કસ આપે છે, જે મોટાભાગના અનૌપચારિક દલીલો કરતા વધારે છે.

કંઇપણ બે વાર સાબિત થયેલ નથી

દરેક લેમ્મા પેનલ સ્થાપિત કરે છે તે તેના પુરાવા સાથે વહેંચાયેલ લેજરમાં જાય છે, તેથી તે ક્યારેય પુનઃઉપજાવવામાં આવતું નથી અને મૃત અંત ક્યારેય પુનઃપ્રયત્ન કરવામાં આવતો નથી. લાંબી સમસ્યાઓ કામ ગુમાવવા વગર અટકાવે છે અને પુન:પ્રાપ્ત કરે છે: ટેબ બંધ કરો અને આવતીકાલે પાછા આવો.