About Theorem.chat
Theorem.chat ગણિતીય દાવો લે છે અને તેને સમાપ્ત કરવાનો પ્રયત્ન કરે છે. તમે દાવો અને તેનો સામનો કરવાનો માપદંડ જણાવો છો. AI મોડેલોની પેનલ - જેટલા તમે ઇચ્છો તેટલા, તમે ઇચ્છો તેવા વેપારીઓમાંથી - તેનો હુમલો કરે છે, અને એક વધુ મોડેલ રીફરે. પછી દલીલ Lean 4 વિરુદ્ધ Mathlib માં ઔપચારિક છે, અને લીન કર્નલ નક્કી કરે છે કે શું તે સાબિત થયેલ છે. છેલ્લું પગલું ઉત્પાદન છે.
કેમ કર્નલ, અને બીજુ મોડેલ નહિં
Ask a model a hard question and you get a fluent answer whether or not it is right. Ask several and they often agree, which feels like corroboration and is not: models share training data and share blind spots. A second model checking the first is still the same kind of judgement, and it can be talked round. The Lean kernel cannot. It either derives the statement from the axioms and Mathlib, or it does not, and confidence has no effect on the outcome.
ઔપચારિક સાબિત કરવા માટેની સામાન્ય રીતને ચકાસવામાં આવે છે અને નકારવામાં આવે છે. સાબિત કરવું કે જે sorry સાથે ખાડાને છોડે છે, એક કે જે native_decide ને અપીલ કરે છે કે જે કર્નલને વિશ્વાસ પર ગણતરી લેવા માટે બનાવે છે, અથવા એક કે જે શાંતિથી નવો અક્ષય રજૂ કરે છે, શોધવામાં આવે છે અને સફળતા તરીકે ગણતરી કરવાને બદલે નકારવામાં આવે છે.
પેનલ ખરેખર શું કરી શકે છે
વાદવિવાદ એ સસ્તો ભાગ છે. પેનલ સાહિત્ય સાથે કામ કરે છે - arXiv, OpenAlex, Crossref - એટલે જાણીતા પરિણામને ખરાબ રીતે ફરીથી મેળવવાને બદલે ઉલ્લેખવામાં આવે છે. તેમાં ગણતરી માટે SageMath અને PARI/GP છે, SMT ઉકેલવા માટે Z3 અને CVC5 છે, OEIS શોધ માટે તે બનાવેલ અનુક્રમને ઓળખવા માટે, અને નેટવર્ક પ્રવેશ વગર સેન્ડબોક્સ પાયથન પર્યાવરણ છે. કોઈપણ તેને સાબિત કરવાનો પ્રયત્ન કરે તે પહેલાં ધારણા દસ હજાર કેસ સામે ચકાસવામાં આવી શકે છે, અને એક વિરોધાભાસી ઉદાહરણ ચર્ચા તરત જ સમાપ્ત કરે છે.
સાક્ષી, બોલી નહિ
જોડણી દલીલ ગુણવત્તા પર સ્કોર નથી. દાવો સ્વીકૃતિ માપદંડોમાં વિભાજિત થાય છે, અને માપદંડ ફક્ત ત્યારે જ સ્થાપિત થાય છે જ્યારે તે પાછળની વસ્તુ ત્રીજી પાર્ટી દ્વારા ફરીથી ચકાસી શકાય છે: સંબંધિત પાસાઓ સાથેનો સ્ત્રોત ઉલ્લેખિત છે, અથવા કોડ જે ખરેખર તેના ખરેખર આઉટપુટ સાથે ચલાવવામાં આવ્યો હતો. ન્યાયદાતા નિયંત્રણ કરતા પહેલા એ સાક્ષીઓને ફરીથી ચકાસે છે, અને તે જોડણી સમાપ્ત થયેલ છે તેવી જાહેરાત કરી શકતો નથી જ્યારે માપદંડ હજુ ખુલ્લો હોય.
તમે પટ્ટી સુયોજિત કરો
માપદંડ પસંદ કરવા માટે તમારો છે, અને રેફરી તેને વાક્યમાં રાખે છે. એક સાવચેત નિષ્ણાત સ્વીકારશે તે માટે પૂછો અને તમે તે મેળવો. દરેક ધારણા સાથે સંપૂર્ણ ડેડ્યુકેટિવ દલીલ માટે પૂછો અને તમે તેના વિરુદ્ધમાં નક્કી થાઓ. પુરસ્કાર સબમિટનો સામનો કરનાર બાર માટે પૂછો, અને સાચા પરિણામ સામાન્ય રીતે પેનલ ક્યાં ટૂંકી પડી તેનું ચોક્કસ ખાતું છે - જે વિશ્વાસપાત્ર દાવા કરતા વધુ મૂલ્યવાન છે તમે તમારે તમારી જાતને ચકાસવી પડશે.
આ વિશે સ્પષ્ટ કરવા માટે: આ મશીન નથી કે જે ખુલ્લી સમસ્યાઓ સમાપ્ત કરે છે. આ મશીન છે કે જે દલીલને સમાપ્ત થયેલ તરીકે પસાર થવા દેવા માટે અનામત રાખે છે જ્યારે તે નહિં હોય, અને તે તમને ચોક્કસપણે કહે છે કે કયું પગલું નિષ્ફળ ગયું.
નિષ્ફળ ઔપચારિકીકરણ એ ઉપયોગી આઉટપુટ છે
જ્યારે લીન સાબિત કરવાનું બંધ નહિ કરે, ત્યારે તમને બાકી રહેલ ચોક્કસ લક્ષ્ય મળે છે. વ્યવહારમાં તે લગભગ હંમેશા એ જ જગ્યા છે જ્યાં અનિવાર્ય દલીલ હાથ વગાડી રહી હતી - દરેક વ્યક્તિએ પ્રસ્તુત આવૃત્તિ વાંચીને પાછળથી નમાવ્યું હશે. આ લક્ષ્ય પછી જે બેઠક પર તેનો હુમલો કરવા માટે શ્રેષ્ઠ રીતે મૂકવામાં આવે છે, તેની સાથે જે પહેલેથી જ પ્રયત્ન કરવામાં આવ્યો છે, અને બીજું કંઈ નથી. મોડેલો જ્યારે અટવાઈ જાય ત્યારે થરથરે છે, પોતાને સંપૂર્ણ ખર્ચે પુનઃસૂચવે છે; એક ચોક્કસ પ્રશ્નને બદલે સામાન્ય રીતે ટોકનોના અડધા ભાગ માટે અવરોધ દૂર કરે છે.
લાંબી કામગીરી જીવંત રહે છે
દરેક લેમ્મા પેનલ સ્થાપિત કરે છે તે તેના પુરાવા સાથે વહેંચાયેલ લેજરમાં જાય છે, તેથી પરિણામો એકવાર લખાયેલ છે અને ક્યારેય પુનઃઉપજાવવામાં આવતા નથી, અને મૃત અંત રેકોર્ડ થયેલ છે તેથી કોઈપણ પાછા તેમની અંદર ચાલે છે. મેચ સર્વર-બાજુ ચલાવે છે અને સાફ રીતે અટકાવે છે - બજેટ પર, પૂરૂં પાડનાર બંધ થવા પર, અથવા કારણ કે તમે ટેબ બંધ કરી છે - અને તેઓ અટક્યા હતા ત્યાં જ પુન:પ્રાપ્ત થાય છે.
આ માટે શું નથી
નિયમ એ એક ધારણા શબ્દ છે. આ સાઇટ ગણિત, તર્ક, સિદ્ધાંતિક કોમ્પ્યુટર વિજ્ઞાન, સિદ્ધાંતિક ભૌતિકશાસ્ત્ર અને આર્થિક સિદ્ધાંત માટે બનાવવામાં આવી છે - ક્ષેત્રો જ્યાં દાવો સાબિત કરવાથી સમાપ્ત થાય છે. જીવવિજ્ઞાન, દવા, રાસાયણિક અથવા સામાજિક વિજ્ઞાનમાં અનુભવવાદી પ્રશ્નો નિયમ ઉત્પન્ન કરતા નથી, તેઓ શોધ ઉત્પન્ન કરે છે, અને કોઈપણ પ્રમાણભૂતતા તેમને નક્કી કરશે. અમારી બહેન સાઇટ referee.chat એ એ જ પેનલ-અને-રેફરીની પ્રક્રિયાને લીન પગલું વગર ચલાવે છે, એવા પ્રશ્નો માટે.