Usho ukuthi ucabangani. I-kernel ikhetha ukuthi iqinisekiswe noma cha.

Ibhodi lemodeli lihlasela izinkinga zakho ngencwadi, SageMath, PARI/GP ne SMT solver, bese libeka imiphumela e Lean 4 versus Mathlib. I-kernel ye-Lean noma i accetta isiqiniseko noma ayisebenzi, futhi akukho inani le-prose ethembekile eshintsha lokho. Uma iphutha uthola inhloso efanele ehlala, evame ukuba lapho isiphakamiso esingasemthethweni siyisandla esihambayo.

Inhloso

Uzokwazi ukuthi yini eyenza ukuthi isebenze. 'Qhubeka noma ngabe X kuyiqiniso, futhi uqinisekise ukuthi 'ishaya' ukhuluma ngaye X'.

Ibha elingacishiswe

Uchwepheshe owaziyo

Izinto ochwepheshe abakwaziyo ezindaweni zabo bazozivumela njengeziqediwe futhi ezilungile.

Isilinganiso sokuthunyelwe

Kuzohlala ukuhlolwa komunye nomunye: yonke inkinga etholakalayo noma ekhishwayo, izindlela ezis…

Ubufakazi obusemthethweni

Ubufakazi obuphelele obuvela empilweni. Isigaba ngasinye siqinisekisiwe, yonke imicabango icaci…

Isilinganiso semali

Ibha yeClay Millennium Prize enikezelwe izobhekana: igcwele, iqukethe, ibonisa ukuthi abameli a…

Isinqumo

Ubufakazi obunembile bokwenza ngokwezimakethe: amathuluzi abiza kakhulu, izingozi ezibizwa ngeg…

Bhala ngiyo

Describe your own standard.

Ummeli ubambe le bar ngokucacile. Buza ubufakazi bemali ephakeme futhi kuzokutshela ngokucacile uma iphaneli iphansi, ngaphezu kokubhekwa kwempumelelo.

Indawo yohlu

Izivakashi eziningi zisho ama-angles amaningi, kanye nezindleko ezingaphezulu ngayinye.

Ummeli

Imithetho ephathelene nemithetho efanele futhi iphinde ibheka yonke ingxenye yeqiniso. Ifanele imodeli yakho enamandla.

Ama-rounds

Izinga lokukhokha

Ukushaya kumisa i-match. Akukho okulahlekile.

Ukubukeka

Yazisa uma kuqediwe

Ubhalise ukuze uqale i-match

Ama-akhawunti amasha athola i-credit yokuqala, eyanele ku-match.

Umhlola ongakaze aqiniseke

Lean 4 nge Mathlib uhlobo-ibheka isibikezelo sokugcina, futhi isiqiniseko ukuthi libhekene sorry, native_decide noma axiom fresh kulahlekile ngaphezu kwamanani. Kuyo: SageMath, PARI/GP, Z3, CVC5 kanye OEIS, ngakho kwakhiwa kungase kucalwe futhi kuphawulwe ngaphambi umuntu ezama ukuveza noma yini mayelana nayo.

Ubufakazi obuhlulekile buyisinqumo

Uma ukwenziwa kwemithetho kungaphumelelanga, inhloso Lean ayikwazi ukuvala idluliselwa kunoma iyiphi indawo engcono kakhulu ebekwe ukuhlasela: kuphela inhloso, hhayi yonke imbali. Ubufakazi obulahlekile bubizwa ngegama lethuba ngokucophelela, okungaphezu kweningi kwezingqinamba ezingaziwa.

Akukho lutho oluqinisekisiwe kabili

Yonke i-lemma indawo yohlu eyenza ihamba kwi-leader ehlukanisiwe neqiniso layo, ngakho-ke ayikho ephinde ivela futhi iziphelo ezifile azikwazi ukuphinde ziphinde zi