Rreth Theorem.chat
Theorem.chat merr një pretendim matematikor dhe përpiqet ta zgjidhë atë. Ti e përcakton pretendimin dhe standardin që duhet të përmbushë. Një panel i modeleve AI - sa të duash, nga cilido shitës që të duash - e sulmon atë, dhe një model tjetër gjykon. Pastaj argumenti formalizohet në Lean 4 kundër Mathlib, dhe kerneli Lean vendos nëse është provuar. Hapi i fundit është produkti.
Pse një kernel, dhe jo një model tjetër
Pyet një model një pyetje të vështirë dhe do të marrësh një përgjigje të rrjedhshme nëse është e drejtë apo jo. Pyete disa dhe ata shpesh bien dakord, që ndjehet si konfirmim dhe nuk është: modelet ndajnë të dhënat e trainimit dhe ndajnë pikat e verbër. Një model i dytë që kontrollon të parën është ende i njëjti lloj gjykimi, dhe mund të flasë rreth tij. Kernel Lean nuk mundet. Ai ose e nxjerr deklaratën nga aksiomat dhe Mathlib, ose nuk e bën, dhe besimi nuk ka efekt në përfundim.
Mënyrat e zakonshme për të falsifikuar një provë formale janë kontrolluar dhe refuzuar. Një provë që lë një vrimë me sorry, një që i bën thirrje native_decide për të bërë kernelin të marrë një llogaritje në besim, ose një që heshtur futet një aksiomë e re, është zbuluar dhe refuzuar në vend që të numërohet si e suksesshme.
Çfarë paneli mund të bëjë aktualisht
Argumentimi është pjesa më e lirë. Paneli punon me literaturën - arXiv, OpenAlex, Crossref - kështu që një rezultat i njohur citohet në vend të ri-derdhur keq. Ka SageMath dhe PARI/GP për llogaritje, Z3 dhe CVC5 për zgjidhjen e SMT, OEIS kërkim për identifikimin e një sekuence që ka ndërtuar, dhe një mjedis Python sandbox me asnjë hyrje në rrjet. Një supozim mund të provohet kundër dhjetë mijë rasteve para se dikush të shpenzojë një raund për të provuar atë, dhe një kundërshembull përfundon diskutimin menjëherë.
Prova, jo eloquencë
Një match nuk vlerësohet në cilësinë e argumentit. Pretendimi shpërbëhet në kriteret e pranimit, dhe një kriter zgjidhet vetëm kur diçka pas tij mund të rikontrollohet nga një palë e tretë: një burim me pasazhin e duhur të cituar, ose kod që është ekzekutuar aktualisht me daljen e tij reale. Arbitri rikontrollon atë provë vetë para gjykimit, dhe nuk mund të deklarojë match të përfunduar ndërsa një kriter është ende i hapur.
Ti e vendose barrën.
Standardi është i juaji për të zgjedhur, dhe gjykatësi e mban atë në kuptimin e fjalës. Kërkoni për atë që një ekspert i kujdesshëm do të pranonte dhe ju merrni atë. Kërkoni për një argument të plotë deduktiv me çdo supozim të deklaruar dhe ju gjykoheni kundër atij në vend. Kërkoni për barin që një çmim do të përballet, dhe rezultati i ndershëm është zakonisht një përshkrim i saktë i asaj ku paneli nuk arriti — që vlenë më shumë se një pretendim i sigurt që ju duhet të kontrolloni vetë gjithsesi.
Për të qenë i qartë rreth kësaj: kjo nuk është një makinë që zgjidh problemet e hapura. Është një makinë që refuzon të lejojë një argument të kalojë si i zgjidhur kur nuk është, dhe që të thotë saktësisht se cili hap dështoi.
Një formalizim i dështuar është rezultati i dobishëm
Kur Lean nuk do ta mbyllë provan, ju merrni objektivin e saktë që mbetet. Në praktikë, ky është pothuajse gjithmonë pika ku argumenti informal ishte duke lëvizur dorën — hapi që të gjithë që lexojnë versionin e prozës do të kishin bërë me kokë. Ky objektiv pastaj i jepet atij vendi që është më mirë i vendosur për ta sulmuar atë, së bashku me atë që është provuar tashmë, dhe asgjë tjetër. Modelet thrash kur janë të bllokuar, duke ripërsëritur veten me koston e plotë; duke kaluar një pyetje specifike në vend të saj zakonisht zhbllokohet për një pjesë të tokeneve.
Punë e gjatë mbijeton
Çdo lemë që paneli vendos shkon në një shënim të përbashkët me provat e tij, kështu që rezultatet janë shkruar një herë dhe kurrë nuk ri-përfshihen, dhe fundjavat janë regjistruar kështu që askush nuk kthehet në to. Matches punon në server dhe ndalon pastër - në buxhet, në një ndërprerje të furnizuesit, ose sepse e mbyllet tab-in - dhe rifillon saktësisht atje ku u ndalua.
Çfarë nuk është kjo për
Teorema është një fjalë deduktive. Ky faqe është ndërtuar për matematikën, logjikën, shkencën teorike kompjuterike, fizikën teorike dhe teorinë ekonomike - fusha ku një pretendim zgjidhet me prova. Pyetja empirike në biologji, mjekësi, kimi apo shkencat shoqërore nuk prodhon teorema, ato prodhojnë gjetje, dhe asnjë sasi formalizimi nuk do t'i vendosë ato. Faqja jonë motër referee.chat përdor të njëjtin proces paneli dhe gjyqtari pa hapin Lean, për pikërisht këto pyetje.