malunga ne-Theorem.chat
Theorem.chat ithatha ityala lezobunzululwazi kwaye izama ukulilungisa. Uchaza ityala, kunye nesimo esifanele ukuba sihlangabezane. Ipaneli yemodeli ye AI - njengeninzi ofuna, ukusuka kunoma ngubani othengisayo ofuna - ihlasele, kunye nenye enye imodeli eyinconywayo. Emva koko isiganeko simiselwe kwi Lean 4 versus Mathlib, kwaye i Lean kernel igqiba ukuba iqinisekisiwe. Lo mhlathi wokuphela yimveliso.
Kutheni i-kernel, kwaye hayi enye imodeli
Umbuzo onzima ubuza imodeli kwaye ufumana impendulo ecacileyo ukuba ilungile okanye ayiyiyo. Umbuzo othile kwaye bavame ukuvuma, oziva ngathi uqinisekiso kwaye akunjalo: imodeli ibelana nge data yoqeqesho kwaye ibelana ngendawo ezimnyama. Imodeli yesibini ekhangela yokuqala ihlala injalo uhlobo lohlolo, kwaye ingathetha phezulu. I Lean kernel ayikwazi. Ivela kwi Mathlib, okanye ayisebenzi, kwaye uxanduva alukho uphawu kwimiphumo.
Iindlela eziqhelekileyo zokudubula ubungqina obusemthethweni zijongwa kwaye zilahliwe. Ubunyani obushiya umngxuma nge sorry, omnye ofuna u native_decide ukwenza i kernel ithathe ubalo kwi trust, okanye omnye ovela ngokulula i axiom entsha, ifunyenwe kwaye ilahliwe endaweni yokubala njengempumelelo.
Izinto eziluncedo
Ungquzulwano luyinxalenye elula. Iqela lisebenza noncwadi - arXiv, OpenAlex, Crossref - ngoko ke impumelelo eyaziwayo ibhalwe ngaphezu kokuphindeka- kuvela kakubi. Inee SageMath ne PARI/GP zokulinganisa, Z3 ne CVC5 ze SMT zosombulula, OEIS ukukhangela ukuchonga ukulandelana okubuyile, kunye nesandboxed Python indawo engenakunikezelwa kothungelwano. Ucinga luya kuhlolwa kwimeko eziliqela ezilishumi ngaphambi kokuba umntu achitha umjikelo efuna ukubonisa, kwaye umzekelo ophikisanayo ugqiba uxoxo ngokukhawuleza.
Ubungqina, hayi ukuthetha
A match ayikho inqaku kwimvelaphi yomgangatho. Ulwazi oluthethwayo luqhutywa ziimfuno zokumkela, kwaye umlinganiselo umiselwe kuphela xa into ecaleni kwayo iyakwazi ukuvavanywa kwakhona yinxalenye yesithathu: umthombo onesiphelo esifanelekileyo esichaziweyo, okanye ikhowudi eyenziwe ngokusemthethweni ngemveliso yayo eyiyo. Umqulunqi uvavanya kwakhona loo bufakazi phambi kokwenza isigqibo, kwaye ayikwazi ukubhengeza ukuba i match igqityiwe ngelixa umlinganiselo uhlala uvulekile.
Umisela ibar
Ixabiso likwindawo yakho yokukhetha, kwaye umqulunqi ugcina ixabiso ngokucacileyo. Buza ukuba yintoni ekufuneka iqela eliqeqeshiweyo liyithathele ingqalelo kwaye ufumana loo nto. Buza ukuba iqela eliqeqeshiweyo lithathele ingqalelo yonke into ekufuneka icaciswe kwaye ufumana uhlolo oluchaseneyo. Buza ukuba ibha ekufuneka inikezelwe iphumelele ijongene nayo, kwaye i-effective honesty ihlala ibonisa ngokucacileyo ukuba iqela lifikelele phi - eli lixabiso elingaphezulu kwegama eliqinisekileyo oza kuhlala ujongene nalo.
Ukuba ucacile malunga nayo: le ayiyiyo isixhobo esigqiba iingxaki ezivuliweyo. Isixhobo esixolela ukuvumela umzekeliso ukuba udlule njengegqibiweyo xa ayiyiyo, kwaye ethetha ukuba ugqibezele inkqubo egqityiweyo.
Ukulungiswa kwenkqubo akuphumelelanga
Xa iLean ingavalanga ubungqina, ufumana injongo echanekileyo ehlala. Kwimisebenzi enjalo, ihlala ikwindawo apho ungquzulwano olungagunyaziswanga luzalise isandla - inkqubo yokufunda wonke umntu uguqulelo lweprosa luza kutyhila ngaphambili. Le njongo ithunyelwe kunoma yiphi indawo efanelekileyo yokuyihlasela, kunye nento ekhe yazama, akukho nto enye. Iimodeli zithasha xa zitshixiwe, ziphinde ziphinde zithi zibiza kakhulu; ukudlula kwemibuzo ekhethekileyo endaweni yoko ihlala ivula i-blocks yenxalenye ye-token.
Umsebenzi omde uhlala
I-lemma nganye ebekwe yipaneli ifika kwi-leader edityaniswe nenyathelo elibonisa, ngoko iziphumo zibhalwe kabini kwaye aziphinde ziphinde zivela, kwaye iziphelo ezifileyo zishicilelwe ukuze akukho mntu ubuyela kuzo. Matches qhuba i-server-side kwaye uphumle ngokucocekileyo - kwi-budget, kwi-provider outage, okanye ngenxa yokuba uvale i-tab - kwaye uqhubeke ngokuchanekileyo apho bagqibe khona.
Izinto eziluncedo
I-theorem yigama elichazayo. Eli phepha libekwe kwi-matematics, logic, theoretical computer science, theoretical physics kunye ne-economic theory - iindawo apho umbuzo ubekwe khona ngokuqinisekileyo. Imibuzo ebonisa ukuqonda kwi-biology, imithi, i-chemistry okanye isayensi yobuhlanga ayivelisi ii-theorems, zivelisa izifundo, kwaye akukho bungakanani bokuba semthethweni obuza kugqiba. Iphepha lethu lenkosikazi referee.chat liqhuba inkqubo efanayo yepaneli kunye nommeli ngaphandle komanyano oluncinci, ngokuchanekileyo kwezi mibuzo.