I-Theorem.chat
Theorem.chat ithatha isinqumo se-mathematics futhi izama ukusixazulula. Usho isinqumo, futhi isilinganiso esifanele kufanele sihlangane. Ibhodi le-AI model — njengeningi njengoba ufuna, kusuka kunoma yimuphi umhlinzeki ofuna — ihlasela, futhi enye imodeli engaphezulu ibheka. Ngemuva kwalokho isiphakamiso sisemthethweni ku-Lean 4 versus Mathlib, futhi i-Lean kernel ikhetha ukuthi iqinisekisiwe. Lo msebenzi wokugcina yimikhiqizo.
Kungani i kernel, futhi hhayi enye imodeli
Umbuzo onzima ubuza imodeli futhi uthola impendulo ecacile ukuthi ngabe ilungile noma cha. Umbuzo othile futhi bavame ukuvuma, okubona njengenqumo futhi akuyona: imodeli ihlanganisa idatha yokuqeqesha futhi ihlanganisa iziqongo ezimnyama. Imodeli yesithathu ehlola yokuqala ihlala ifana nesimo sesinqumo, futhi ingaxoxwa phezulu. I-Lean kernel ayikwazi. Ithola isibikezelo kusuka ku-axioms ne-Mathlib, noma ayikwenzanga, futhi ukuphepha akuyona inkinga yemiphumela.
Izindlela ezijwayelekile zokukhangisa isiqiniseko esisemthethweni zihlolwe futhi zilahlekile. Isiqiniseko esishiya i-hole ne-sorry, esidinga i-native_decide ukuze i-kernel ithathe ukulinganisa ngokuthembela, noma esifaka ngokucophelela i-axiom entsha, sitholakalela futhi silahlekile ngaphezu kokubhekwa njengempumelelo.
Izinto lapho indawo yohlu ingakwenza khona
Ukukhuluma kungenxa yengxenye ebiza kakhulu. Ipanel isebenza ngencwadi — arXiv, OpenAlex, Crossref — ngakho-ke imiphumela eyaziwayo ibhalwe ngaphezu kokukhishwa kabusha. I-SageMath ne-PARI/GP isetshenziswa ukulinganisa, i-Z3 ne-CVC5 isetshenziswa ukuxazulula i-SMT, i-OEIS isetshenziswa ukulinganisa ukulandelelana okusha, ne-sandboxed Python environment engenayo ukungena kwenethiwekhi. Umbono ungahlolwa ngezinkinga ezingu-10,000 ngaphambi kokuba umuntu asebenzise umjikelezo wokufuna ukukhombisa, futhi isibonelo esiphikisanayo siphelile ukukhuluma ngokushesha.
Ubufakazi, hhayi ukucasuka
A match ayikho i-score ehlobene nekhwalithi yezingqinamba. Ubufakazi buhlukaniswa zibe izimo zokuvunyelwa, futhi isimo sizomiswa kuphela uma kukhona okuthile ngasemva kwayo kungaphinde kuhlolwe kabusha yingxenye yesithathu: umsuka nengxenye efanele ebhalwe, noma ikhodi eyenziwe ngokusemthethweni ne-output yayo engokoqobo. Ummeli uphinde ubheka ukuthi isithombe silungile ngaphambi kokwenza isinqumo, futhi akufanele imemezele i-match iqediwe ngenkathi isimo sikhona.
Ubeka ibha
Izinga liwukhetho lwakho, futhi ummeli ugcina ngokucacile. Buza ukuthi yini ochwepheshe owaziyo ongeke avume futhi uthola lokho. Buza ubufakazi obuphelele obunombono ophelele nganoma yisiphi isiqiniseko esishoyo futhi uthola ukucwaswa ngalokho endaweni. Buza ibha yokulethwa kwemali ezoba nezinkinga, futhi imiphumela ethembekile ivame ukuba ne-akhawunti ecacile lapho ipaneli idlula khona - ebiza kakhulu kunecala eliqiniseke ukuthi uzodinga ukubhekana nalo.
Ukwenza kube lula: lokhu akuyona imishini exazulula izinkinga ezivulekile. Imishini ephikisana nokuvumela isiphakamiso sidlule njengesixazululwe uma kungekho, futhi lokho kuzokutshela ngokucacile ukuthi iyiphi inqubekela phambili ehlulekile.
Ukulungiswa okungaphumelelanga kuyisixazululo esisebenzayo
Uma Lean ngeke ivala isiqiniseko, uthola inhloso efanele ehlala. Emisebenzini ukuthi cishe njalo indawo lapho isiphakamiso engekho emthethweni wabe isandla-waving - isinqumo wonke umuntu ufunde inguqulo proza uzobe nodded ngaphambili. Le njongo bese idluliselwa kunoma iyiphi isikhala engcono kakhulu ebekwe ukuhlasela, kanye nento eselokhu esebenza, futhi akukho lutho olunye. Amamodeli thrash lapho baphumile, reiterating ngokwabo ngezindleko ezigcwele; ukudlula imibuzo eyodwa ekhethekile endaweni ngempela unblocks for a fraction of the tokens.
Umsebenzi omde uhlala
Yonke i-lemma iphaneli esungula ihamba kwi-leader ehlukanisiwe neqiniso layo, ngakho-ke izimpendulo zibhalwe kabili futhi akufanele ziphinde zithathwe, futhi iziphetho ezifile zirekhodwa ukuze akukho muntu ohamba emuva kuzo. Matches yenza ikhasimende-ikhasimende futhi ubeke isikhathi eside ngokucophelela — ngemali, nge-ohlinzeki ongekho, noma ngoba uvale i-tab — futhi uqhubeke ngokucophelela lapho bavala khona.
Izinto ezingaba khona
I-theorem yigama elichazayo. Le ndawo ifakwe i-matematics, logic, i-theory computer science, i-theory physics ne-economic theory — izimboni lapho icala libekwe khona ngokuveza. Imibuzo ehlobene ne-empirical empilweni, ukwelashwa, ukhemikhali noma izifundo zomphakathi ayikhiqizi i-theorems, ikhiqiza izimpendulo, futhi akukho inani lokungabaza kuzozixazulula. I-site yethu yowesifazane referee.chat isebenza ngendlela efanayo yepanel-and-referee ngaphandle kwe-Lean step, ngokucacile kwalezi mibuzo.