Kwụsị n'ihe a na-ekwu. Kọlọn ahụ na-ahọrọ ma ọ bụrụ na ọ bụ ihe a na-egosi.

Paneelụ nke ụdị na-abịa n'ihe mgbu gị na akwụkwọ akụkọ ihe mere eme, SageMath, PARI/GP na SMT solver, mgbe ahụ na-eme ka ihe pụta ìhè na Lean 4 megide Mathlib. Lean's kernel ma na-anabata ihe àmà ma ọ bụ ọ bụghị, na enweghị ọnụọgụgụ nke n'aka na-agbanwe agbanwe na. Mgbe ọ na-akwụsị ị ga-enweta ihe n'aka na-abịa, nke bụ mgbe niile ebe ajụjụ na-enweghị isi bụ aka-waving.

Nhazi

Biko kọwaa ihe e merela. 'Depụta ma X bụ eziokwu, na gosi na ọ na-emetụta 'gwa m banyere X'.

Báà nke ọ ga-ehichapụ

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.

Onye na-ekpe ikpe na-echekwa bar a n'ụzọ litirịrị. Biko maka ngosipụta nke nhọpụta na ọ ga-agwa gị n'ụzọ doro anya mgbe paneelụ na-apụ n'okpuru, kama ịgwa gị na ọ ga-abịa.

Paneelụ ahụ

Ụlọ ndị ọzọ pụtara ìhè na ọbụna ọnụọgụgụ ndị ọzọ, nakwa ọnụọgụgụ ndị ọzọ n'otu n'otu.

Nhazi

Nhazi na nhazi na-echegharị ihe niile nke ihe ngosipụta. Ọ bara uru maka ụdị gị kasị ike.

Òtù

Oge n'ime

Ịgba ya n'oge na-emechi mmem. Enweghị ihe ọbụla a hụla.

Nhazi

Bipụta mgbe e mechara

Nweta ndebanye iji malite mmeri

Akaụntụ ọfụụ na-enweta kredit nke mbụ, nke dị n'aka maka mmeri n'eziokwu.

Nlekọta ahụ agaghị ekwe omume ikwe ka ọ bụrụ

Lean 4 na Mathlib ụdị-chekwaa nke ikpeazụ statement, na a proof nke leans na sorry, native_decide ma ọ bụ ọhụrụ axiom bụ hapụ n'ihi na na-ejide. N'ebe ya: SageMath, PARI/GP, Z3, CVC5 na OEIS, otú a arụ ọrụ nwere ike na-enyocha na-akọwa tupu onye ọ bụla na-achọ ịnye ihe ọ bụla banyere ya.

A faịlụ proof bụ a finding

Mgbe formalization na-akwụsị, ihe n'ime Lean nwere ike ịkwụsịghị akwụsị na-abịa n'ebe ọbụla nke dị mma iji banye ya: naanị ihe n'ime ahụ, ọ bụghị akụkọ ihe mere eme niile. N'ihe n'ime ahụ a hapụghị aha nke agwa, nke bụ ihe dị ka ihe n'ime ihe ndị a na-emekarị.

Ihe ọbụla a na-egosi ugboro abụọ

Lemma ọbụla paneelụ na-eguzobe na-aga n'ime leedger mejupụtara na nkwenye ya, yabụ ọ gaghị adị n'ọdịnihu ma ọ gaghị adị n'ọdịnihu. Nchegbu ogologo na-akwụsị na-aga n'ihu na-enweghị igbu ọrụ: mechie táàbụ̀ ma bịaghachi n'ọdịnihu.