Ku saabsan Theorem.chat
Theorem.chat qaadaa dalab xisaab iyo isku dayaya in ay ka soo bixi. Waxaad sheegtaa dalab, iyo heerka ay leedahay in ay la kulmaan. A guddiga AI qaabab — sida badan oo aad rabto, ka mid ah iibsadayaasha aad rabto — weerarka, iyo mid ka badan oo qaabka xubnaha. Markaas, doodda waxaa formalized in Lean 4 ka dhanka ah Mathlib, iyo kernel Lean go’aansada haddii ay la xaqiijiyay. In tallaabada ugu dambeysay waa wax soo saarka.
Maxaa kernel ah, iyo ma qaab kale
Su’aalo qaar ka mid ah oo ay si joogto ah u ogolaadaan, taas oo u muuqataa sida xaqiijinta iyo ma aha: models qaybsadaan xogta tababarka iyo qaybsadaan meelaha blind. A qaabka labaad ee tijaabinta ugu horeysay waa weli la mid ah noocyada xukun, oo waxaa la wadaagi karaa wareegga. The Lean kernel ma awoodi karo. Waxay ama ka soo baxa warbixinta ka axioms iyo Mathlib, ama ma, iyo kalsoonida ma saameyn ku yeelan wax natiijo ah.
Hababka caadiga ah ee been abuurka caddayn rasmi ah ayaa la hubiyo oo la diiday. A caddayn oo ka tagay dhul la sorry, mid ka mid ah oo ka dalbaday native_decide in ay kernel qaadaan xisaabinta ku kalsooni, ama mid ka mid ah oo si xasilan u soo bandhigay axiom cusub, waxaa la ogaadaa oo la diiday in ka badan in ay tiradoodu sida guusha.
Waxa panelka dhab ahaantii samayn kara
Xukuumadda waxay la shaqeysaa buugaagta - arXiv, OpenAlex, Crossref - sidaas darteedna natiijo la yaqaan ayaa lagu xusay in ka badan in dib loo soo celiyo si xun. Waxay leedahay SageMath iyo PARI/GP xisaabinta, Z3 iyo CVC5 SMT xallinta, OEIS loo hubiyo in ay aqoonsadaan silsilad ay dhistay, iyo sandboxed Python deegaanka aan la xiriirin network. A saadaasha waxaa lagu tijaabi karaa ka hor toban kun oo kiis ka hor qof kasta oo ku bixiyaan wareegga isku dayaya inay muujiyaan, iyo counterexample dhamaystiran wada hadalka si deg deg ah.
Xujo, ma aha hadalka
A match ma aha mid ku guuleystay on argument tayada. Dacwadda waa la kala qaybiyay in shuruudaha aqbalaadda, iyo shuruudaha waa kaliya la go'aamiyay marka wax ka dambeeya ay noqon kartaa dib-u-eegista by dhinac saddexaad: a source with the relevant passage quoted, ama code in dhab ahaantii la fuliyay la soo saarka dhabta ah. The arbitrator dib-eegista in caddayn isaga ka hor go'aan, oo ma awoodo in ay ku dhawaaqaan in match dhamaatay inta shuruudaha weli waa furan.
Waxaad ku siin bar
Qiimaynta waa adiga kuu ah in ay doortaan, iyo garsooruhu waa uu leeyahay si dhab ah. Su'aalo waxa xirfadle xiiso leh aqbali lahaa oo aad ka heli. Su'aalo ee doodda deductive buuxa la aaminsan yahay oo dhan oo aad ka heli ka hor maxkamadda in ay ka. Su'aalo barka abaalmarinta soo gudbinta la kulmi lahaa, iyo natiijada run ah waa caadi ahaan xisaab dhab ah oo meesha guddiga hoos u dhacay gaaban — taas oo ka qiimo badan in ay sheegasho kalsooni aad u baahan tahay inaad isbarbar dhigto si kastaba ha ahaatee.
Si ay u fududahay oo ku saabsan: tani ma aha mashiin oo xal u tahay dhibaatooyinka furan. Waa mashiin oo diido in ay siiyaan doodda u gudbaan sida ay go’aan ka gaareen marka ay tahay in aan, iyo in uu kuu sheego si toos ah oo tallaabo ku fashilantay.
A formalization ku fashilantay waa natiijada faa'iido leh
Marka Lean ma xiran doono caddayn, waxaad heshaa ujeedka saxda ah ee sii joogaya. Dhaqdhaqaaqa in waa in aad u badan tahay mar walba meesha ay doodda aan rasmi ahayn ahaa gacanta-wax-dhaqaaqaya — tallaabada qof kasta oo akhriya version suugaanta lahaa uun la soo dhaafay. In goal waa in markaas la siiyo mid kasta oo kursiga ugu fiican ee lagu soo bandhigay in ay weeraraan, oo ay la socdaan waxa horey loo isku dayay, iyo waxba kale.
Long shaqada nool
Matches socda server-ga dhinac iyo joojin si nadiif ah - on miisaaniyadda, on provider off, ama sababtoo ah waxaad xidhay tab - iyo sii wadaan si toos ah halkaas oo ay joojiyeen.
Maxaa tani ma aha
Theorem waa eray deductive. Site this waa la dhisay si ay xisaabta, loox, sayniska kombiyuutarka aragtida, fiisikis aragtida iyo aragtida dhaqaalaha - goobaha halkaas oo dacwad waa la xalin karaa caddayn. su'aalaha empirical ee biolojiga, daawada, kiimikada ama cilmiga bulshada ma soo saaraan theorems, waxay soo saaraan natiijooyinka, iyo wax lacag ah oo formalization iyaga go'aan ka gaari doonaa. Our sister site referee.chat socda habka panel-iyo-referee isku mid ah aan tallaabada Lean, si ay su'aalahaas.