E pā ana ki te Theorem.chat
Theorem.chat e mau ana i tētahi kīanga pāngarau me te whakamātau ki te whakatau i a ia. E kī ana koe i te kīanga, me te paerewa me te tūmanako kia tūmanako ai. He rōpū tauira AI — he maha pēnei i te mea e hiahiatia ana e koe, mai i ngā kaipāpāho e hiahiatia ana e koe — e whakaeke ana i a ia, me tētahi tauira anō e whakatūpato ana. Kātahi ka whakamātauria te tautohe i roto i te Lean 4 ki te Mathlib, ā, ka whakatau te karihi Lean mēnā ka whakamātauria. Ko te hipanga whakamutunga te hua.
He aha te karihi, ā, kāore tētahi atu tauira?
E pātai ana ki tētahi tauira ki tētahi pātai uaua, ā, ka whiwhi i tētahi whakautu mārama mēnā e tika ana, kāore rānei. He maha ngā pātai, ā, he rite tonu te whakaae, e āhua ana he whakaū, ā, kāore: ka tiritiri ngā tauira i ngā raraunga whakaakoranga me te tiritiri i ngā wāhi matapōkere. Ko te tauira tuarua e arotake ana i te tuatahi, he ōrite tonu te āhua o te whakatau, ā, ka taea te kōrero i te hurihanga. Kāore e taea e te karihi Lean. Ka puta mai rānei i te kīanga mai i ngā āhuahira me te Mathlib, kāore rānei, ā, kāore he pānga ki te hua.
Ko ngā tikanga noa iho hei whakawātea i tētahi whakaaturanga tika e whakamātautia ana, e whakakāhoretia ana. He whakaaturanga e waiho ana i tētahi porohita me te sorry, tētahi e whakahau ana ki te native_decide hei mahi i te karihi ki te whakawātea i te tatau i runga i te whakapono, tētahi rānei e whakamōhio ana i tētahi āhua hōu, ka kitea, ā, ka whakakāhoretia, kaua e tatau hei angitu.
Ko te mea e taea e te taupoki te mahi
Ko te tautohetohe te wāhanga ngāwari. Ka mahi te taupuni ki ngā pukapuka — arXiv, OpenAlex, Crossref — kia whakahuatia ai tētahi hua mōhiotia, kaua e whakawāteatia. He SageMath me te PARI/GP mō te tātaitanga, he Z3 me te CVC5 mō te whakaoti SMT, he OEIS ki te kite i tētahi raupapa kua hangaia, me tētahi taiao Python kāore i te āhei ki te rārangi. Ka taea te whakamātautau i tētahi whakaaro ki ngā take tekau mā tekau i mua i te wā e whai ana tētahi tangata i tētahi hurihanga e ngana ana ki te whakamātau i te mea, ā, ka whakamutua e tētahi tauira whakakore te kōrero i te wā kotahi.
Ko te whakaaturanga, ehara i te whakamātautautanga
Kāore e whakawāteatia te ōritetanga i runga i te āhuatanga o te tautohe. Ka whakawāteatia te kīanga ki ngā paearu whakaaetanga, ā, ka whakatau anake tētahi paearu ina taea te arotake anō tētahi mea i muri i a ia e tētahi wāhanga tuatoru: he pūtake me te whakawhitinga whai tikanga, he waehere rānei i whakawāteatia i te huaputa tūturu. Ka arotake anō e te kaiwhakangahau te whakaaturanga i mua i te whakatau, ā, kāore e taea te whakapuaki i te ōritetanga i te wā e tūwhera tonu ana te paearu.
Kua tautuhia e koe te pae
Ko te paerewa ko tātou ki te kōwhiri, ā, ko te kaiwhakakōrero e pupuri ana i te kupu. E pā ana ki te mea e whakaae ana te tohunga mātauranga, ā, ka whiwhi rātau ki taua mea. E pā ana ki tētahi tautohe whakawhāiti katoa me ia whakaaro e kīia ana, ā, ka whakataua koe ki taua mea. E pā ana ki te pae e anga ana te tono utu, ā, ko te hua pono he pūkete tika o te wāhi i pōturi ai te tauwāhi - he nui ake te uara i tētahi kīanga ā-whakaaro me tātai ki a koe.
Hei whakamārama i tēnei: ehara tēnei i tētahi mīhini e whakaoti ana i ngā raruraru tūwhera. He mīhini e whakakāhore ana i te whakaaetanga ki tētahi tautohe hei whakaoti i te wā kāore, ā, ka kī mai ki a koe i te wā i pōturi ai te hipanga.
Ko te huaputa whai hua te whakakōrero kāore i angitu.
Ki te kore e kati te Lean i te whakaaturanga, ka whiwhi ki te whāinga tika e toe ana. I te mahi, tata tonu ki te wāhi i whakawāteatia ai te tautohe ā-ringa - ko te hipanga ka whakamātautia e ia e te hunga katoa e ako ana i te putanga tātai. Ka tukua taua whāinga ki tētahi tūru e pai ana ki te whakaeke i a ia, tae atu ki te mea kua whakamātauria kētia, ā, kaore he mea atu. Ka pōturi ngā tauira ina pāngia rātau, e whakawātea ana i a rātau i te utu katoa; ko te whakawhitinga i tētahi pātai motuhake i te nuinga o te wā ka whakawāteatia mō tētahi hautanga o ngā tohu.
E ora ana te mahi roa
Ko ia lemma e whakatūria ana e te taupoki e haere ana ki tētahi pūkete tiritiri me tōna whakaaturanga, kia tuhituhi ai ngā hua kotahi, kāore anō kia tāruatia, ā, ka whakatūtūtia ngā mutunga kore, kia kore ai e haere anō tētahi ki roto i a rātou. Ka haere ngā whakahoahoa i te taha hoapā, ā, ka whakamutua mārō — i runga i te pūtea, i te whakakoretanga o te kaiāwhina, nā te mea rānei i katia e koe te tāpa — ā, ka haere tonu i te wāhi i whakamutua ai rātau.
He aha tēnei mō
Ko te kupu whakawhāiti te kupu whakawhāiti. Ka hangaia tēnei pae mō te pāngarau, te arorau, te pūtaiao rorohiko ā-ariā, te ahupūngao ā-ariā, me te ariā ohaoha — ngā āpure e whakatauria ana he kīanga e te whakaaturanga. Kāore ngā pātai ā-whakapae i roto i te koiora, te rongoā, te matū, te pūtaiao pāpori rānei, kāore e whakaputa i ngā tautuhinga, ka whakaputaina e rātou i ngā kitenga, ā, kāore he nui o te whakamātautau e whakatau ai i a rātou. Ko tātau pae hoa referee.chat e whakahaere ana i te tukanga pane me te kaiwhakakōrero ōrite me te kore e whai i te hipanga Lean, mō ēnei pātai.
referee.chat — te ariā ōrite, mō ngā kerēme ā-whakamātautau.