Theorem.chat inguru.
Theorem.chatk aldarrikapen matematiko bat hartzen du eta konpontzen saiatzen da. Zuk aldarrikapena adierazten duzu, eta bete behar duen estandarra. AI modeloen panel batek - nahi duzun zenbat, nahi duzun saltzailetik - erasotzen du, eta modelo epaile bat gehiago. Gero argudioa Lean 4an formalizatu egiten da Mathliben aurka, eta Lean kernelak frogatzen den ala ez erabakitzen du. Azken pauso hori da produktua.
Zergatik kernel bat, eta ez beste modelo bat
Modelo bati galdera zaila egin eta erantzun zuzena edo okerra jasotzen duzu. Zenbait galdetu eta askotan ados jartzen dira, baieztapen gisa sentitzen dena, baina ez da hala: modeloek entrenamendu-datuak eta puntu itsu-datuak partekatzen dituzte. Lehenengoa egiaztatzen duen bigarren modeloa epaiketa mota bera da, eta hitz egin daiteke. Lean kernelak ezin du. Adierazpena axiomak eta Mathlib-tik erauzten du, edo ez, eta konfiantzak ez du emaitzan eraginik.
Proba formal bat faltsutzeko ohiko moduak egiaztatu eta baztertu egiten dira. sorry-ekin zulo bat uzten duen froga bat, native_decide-ri dei egiten dion froga bat kernelak konfiantzaz konputatu dezan, edo axioma berri bat isilpean sartzen duen froga bat, detektatu eta baztertu egiten da arrakasta bezala zenbatu beharrean.
Panelak benetan egin dezakeena
Eztabaidatzea da zati merkeena. Panelak literaturarekin lan egiten du - arXiv, OpenAlex, Crossref - beraz emaitza ezaguna aipatzen da gaizki berrerabiliz baino. SageMath eta PARI/GP ditu konputaziorako, Z3 eta CVC5 SMT ebazteko, OEIS bilaketa eraikitako sekuentzia identifikatzeko, eta sandbox Python ingurunea sare sarbiderik gabe. Konjetura bat hamar mila kasutan probatu daiteke inork frogatzen saiatzen den bitartean, eta kontra-adierazpen batek berehala amaitzen du eztabaida.
Ebidentzia, ez elogioa
Bat-egite bat ez da puntuatzen argumentuaren kalitatearen arabera. Egiaztapena onarpen-irizpideetan banatzen da, eta irizpide bat bakarrik ebazten da atzean dagoen zerbait hirugarren batek berriro egiazta dezakeenean: iturburu bat pasadizo egokia aipatuz, edo benetan exekutatu zen kodea bere benetako irteerarekin. Epaileak froga hori berraztertzen du erabaki aurretik, eta ezin du parekatzea bukatutzat eman irizpidea irekita dagoen bitartean.
Zuk jarri duzu araua.
Zuk aukeratu behar duzu estandarra, eta epaileak literalki hartzen du. Eskatu aditu kontutsu batek onartuko lukeena eta horixe jasoko duzu. Eskatu argudio deduktibo osoa, suposizio guztiak adierazita, eta horren aurka epaituko zaituzte. Eskatu sari bat aurkezteko behar den maila, eta emaitza zintzoa panelak zertan huts egin zuenaren azalpen zehatza izaten da normalean - horrek balio handiagoa du zuk zeuk egiaztatu beharko zenukeen aldarrikapen konfidentziala baino.
Argi eta garbi esateko: hau ez da irekita dauden arazoak ebazten dituen makina bat. Argumentu bat ebatzita ez dagoenean ebatzita bezala pasatzeari uko egiten dion makina bat da, eta zehazki esaten dizu zein pausok huts egin duen.
Huts egin duen formalizazioa da irteera erabilgarria
Lean-ek froga ixten ez duenean, geratzen den helburu zehatza lortzen duzu. Praktikan, ia beti argumentu informala eskua mugitzen ari zen lekua da - prosa bertsioa irakurtzen duen edonork burua altxatuko lukeen urrats hori. Helburu hori, orduan, erasotzeko lekurik onena duenari ematen zaio, jadanik saiatu denarekin batera, eta beste ezer ez. Ereduak blokeatuta daudenean, kostu osoan berragertzen dira; galdera zehatz bat pasatzeak, normalean, blokeoa kentzea eragiten du tokenen zati baten truke.
Lan luzeak irauten du
Panelak ezartzen duen lema bakoitza, bere frogarekin batera, liburu partekatu batean sartzen da, beraz, emaitzak behin idatzi eta ez dira inoiz berriro deribatzen, eta bidegabekeriak erregistratzen dira, inork ez dezan itzuli. Bat-etorriek zerbitzari-aldea exekutatzen dute eta garbi gelditzen dira — aurrekontuagatik, hornitzaile bat gelditu delako edo fitxa itxi duzulako — eta gelditu ziren lekutik bertatik jarraitzen dute.
Zertarako ez da hau?
Teorema hitz deduktiboa da. Gune hau matematika, logika, informatika teorikoa, fisika teorikoa eta teoria ekonomikoarentzat eraiki da, alegia, froga baten bidez baieztapen bat ebazten den eremuak. Biologia, medikuntza, kimika edo gizarte zientzietako galdera enpirikoek ez dituzte teoremak sortzen, aurkikuntzak sortzen dituzte, eta ez dute formalizazio kopuru handirik behar erabakiak hartzeko. Gure ahizpa den referee.chat guneak panel- eta epaimahai-prozesu bera exekutatzen du Lean urratsik gabe, galdera horietarako zehazki.