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

Careful expert

What a competent professional in the field would accept as done and correct.

Publication standard

Would survive peer review: every claim sourced or derived, methods stated, limitations acknowle…

Formal proof

A complete deductive argument. Every step justified, every assumption stated, no appeals to pla…

Prize standard

The bar a Clay Millennium Prize submission would face: a complete, self-contained, gap-free pro…

Decision-grade

Enough evidence to act on commercially: options costed, risks named, recommendation justified.

Write my own

Describe your own standard.

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

Whakaputanga ina oti

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ā.