Ka whakapuakina te kerēme. Ka whakatau te karihi mēnā ka whakamātauria.

Ko tētahi taupānga tauira e whakaeke ana i tō tātau raruraru me te pukapuka, SageMath, PARI/GP me tētahi kaiwhakangahau SMT, kātahi ka whakaritea te hua ki te Lean 4 ki te Mathlib. Ka whakaae te karihi o Lean ki te whakaaturanga, kāore rānei, ā, kāore he nui o te whakamātautau e huri ana i taua mea. Ki te pōturi, ka whiwhi ki te whāinga tika e toe ana, i te nuinga o te wā ka whakawāteatia te tautohe ā-ringa.

Ko te whāinga
He tino mārama ki te tikanga o te mahi. 'Ka whakatau mēnā he pono X, ā, ka whakaaturia he 'pāpāho' e kōrero ana ki a au mo X'.
Ko te pae me whakamātauria
E pupuri ana te kaiwhakakōrero i tēnei pā. E tono ana mō tētahi whakaaturanga taumata-whakahaere, ā, ka kī mai mārama ki a koe ina pōturi te taupuni, kaua e kī i te wikitoria.
Te taupānga
Ko te tikanga o ngā tūru kē atu he nui ake ngā koki, ā, he nui ake te utu i ia huri.
Te kaiwhakawa
Ka whakaritea ngā ture i runga i ngā paerewa me te arotake anō i ia wāhanga o te whakaaturanga. Ko te tikanga kia kaha rawa atu tō tātou tauira.
Roto
Te tepe o te utu
Ka whakamutua te pāpāho mā te pāpāho. Kāore he mea ngaro.
Te āhua o te mārama
Ka whakaingoatia te whakatūnga o te pāpāho
Ka whiwhi ārai tīmata ngā kāri hōu, he nui rawa mō tētahi ōritetanga tūturu.
He kaitirotiro kāore e taea te whakahauhau

Ko te Lean 4 me te Mathlib e whakamātau ana i te kīanga whakamutunga, ā, ko tētahi whakaaturanga e whakawhirinaki ana ki te sorry, native_decide, he āhua hōu rānei, ka whakakāhoretia, kaua e tatautia. I te taha o tēnei: SageMath, PARI/GP, Z3, CVC5 me te OEIS, nō reira ka taea te tātaitai me te tohu i tētahi hanganga i mua i te whakamātautanga o tētahi tangata ki te whakamātau i tētahi mea mō ia.

He kitenga te whakaaturanga whakakore.

Ki te kore te whakatinanatanga i te whakatūpato, ka tukua te whāinga kāore i taea e Lean te kati ki tētahi tūnga pai rawa hei whakaeke i a ia: ko taua whāinga anake, ehara i te hītori katoa.

E rua nga wā e whakamātau ana te mea katoa

Ko ia rārangi i whakatūria e te papa ka haere ki tētahi pūrākau tiritiri me tōna whakaaturanga, nā reira kāore anō kia tāruatia, ā, kāore anō kia whakamātau anō ngā mutunga kore. Ka whakamutua ngā raruraru roa, ā, ka haere anō me te kore e ngaro te mahi: ka kati te tāpa, ka hoki anō i te rā.