Theorem.chat-нан астам
Theorem.chat математикалық мәліметті алып, оны шешуге тырысады. Сіз мәліметті, оның сәйкес келетін стандартын келтіресіз. ДНҚ модельдерінің тобының - қалағаныңызша, қалағаныңызша өндірушілердің - оны шабуылдап, тағы бір модельді шешеді. Содан соң, аргумент Lean 4- ден Mathlib- ке дейін формализацияланады, Lean өзегі оның дәлелдене ме, жоқ па дегенді шешеді. Соңғы қадамы - нәтиже.
Неліктен өзегі, ал басқа модель емес
Модельге қиын сұрақ қойып, дұрыс па, дұрыс емес пе деген сұраққа жауап бересіз. Бірнеше сұрақ қойып, олар көбіне келіседі, бұл әдетте, дәлелдеу сияқты, бірақ ол емес: модельдер оқыту деректерді және қараңғы жерлерді бөліседі. Екінші модельде біріншісін тексеру әлі де сол сияқты, бұл туралы әңгімелесуге болады. Lean өзегі олай істемейді. Ол аксиомалардан және Mathlib- ден мәліметті алады, немесе ол жоқ, және сенімділік нәтижеге әсер етпейді.
Регламентті дәлелдеудің әдеттегі жалған тәсілдері тексеріліп, қабылданбайды. sorry- ге тесік қалдырған, өзегіне сенімділікпен есептеу жасауға мәжбүрлеген native_decide- ге шағымданған, немесе жаңа аксиоманы жымиып енгізген дәлелдеулер байқалып, сәтті деп есептелмей, қабылданбайды.
Панельдің нақты істей алатын әрекеттері
Сұрақ- жауап - бұл арзан нұсқа. Панель әдебиеттермен жұмыс істейді - arXiv, OpenAlex, Crossref - сондықтан белгілі нәтижелерді қайталаудан гөрі, олар келтіріледі. Ол есептеу үшін SageMath және PARI/GP, SMT шешу үшін Z3 және CVC5, құрылған тізбекті анықтау үшін OEIS, желіге қосылусыз Python ортасы бар. Сұрақ- жауапты ешкім дәлелдеу үшін бір айналым өткізбей он мың жағдаймен сынап көруге болады, ал қарсы мысалмен әңгіме бірден аяқталады.
Дәлел, сөз шеберлігі емес
Түйістік аргументтердің сапасына қарай бағаланбайды. Сұрау қабылдау критерийіне бөлінеді, критерий тек үшінші тараптың көмегімен қайта тексерілсе ғана шешіледі: көзі келтірілген дәйексөз, немесе шын орындалған коды, оның шын шығысы. Рефери шешім қабылдар алдында осы дәлелдерді қайта тексереді, критерий ашық тұрғанда сәйкестік аяқталды деп жариялай алмайды.
Сіз баптайсыз
Стандартты таңдау сіздің қолыңызда, ал судья оны сөзбе-сөз ұстайды. Еңбекқор маман қабылдайтын стандартты сұраңыз, сонда сіз оны аласыз. Әрбір болжаммен толық дедуктивті аргумент сұраңыз, сонда сіздің орнына сол аргументке сәйкес сізге үкім шығарылады. Жүлдеге ұсынылған жұмыстың талаптарын сұраңыз, онда шынайы нәтиже әдетте панельдің не үшін кемшілік жасағанын дәл көрсетеді - бұл өзіңіз тексеруіңіз керек деген сенімді мәлімдемеден артық.
Ашық айтайын: бұл ашық мәселені шешетін машина емес. Бұл шешілмеген аргументті шешілген деп қабылдамайтын машина, және ол қай қадамы қате болғанын дәл айтып береді.
Формалдау қатесі - пайдалы шығыс
Lean дәлелдеуін жаба алмаса, қалған мақсатты табасыз. Практикада бұл әрқашан да бейресми пікірталастың қол шапалақтауы болып табылады - бұл қадамды барлық оқырмандар прозалық нұсқасын оқып болған соң, басын иіп, тоқтап қалады. Содан соң бұл мақсатты басқа ештеңесіз, тек қана әлі қолданылған нәрселермен бірге, шабуылдауға ең лайықты орынға беріледі. Модельдер тоқтап қалса, өздерін толық бағамен қайталап, тоқтап қалады; оның орнына бір сұрақты дұрыс жауап берсе, әдетте, текшелердің бір бөлігі үшін блоктауды шешеді.
Ұзақ жұмыс сақталады
Панель анықтаған әрбір лемма өзінің дәлелімен бірге ортақ журналға жазылады, сондықтан нәтижелер бір рет жазылып, қайта алынбайды, ал тоқтап қалғандар жазылып, ешкім қайта оралмайды. Сервер жағынан орындалатын сәйкестіктер бюджетке, провайдердің тоқтап қалуына немесе қойындыны жабғаныңызға байланысты тоқтап, содан кейін тоқтап тұрған жерінен қайта басталады.
Бұл не үшін емес
Теорема деген сөз дедуктивті сөз. Бұл сайт математика, логика, теориялық информатика, теориялық физика және экономикалық теория салалары үшін жасалған, бұлар дәлелдеу арқылы шешілетін салалар. Биология, медицина, химия немесе әлеуметтік ғылымдардағы эмпирикалық сұрақтар теоремаларды емес, нәтижелерді береді, оларды қандай да бір формализация шешпейді. Біздің referee.chat деген жақын сайтымыз осы сұрақтарға Lean қадамсыз, панель және референт процесін қолданады.