Nhazi ọrụ
1. Ihe ọrụ ahụ na-eme
Ị na-enye a n'ihu na a standard. Anyị na-agba ya n'ihu a panel nke AI models ị họrọ, na-agbakwunyere a n'ihu model na-achịkwa na-anabata criteria, na anyị na-achọ ka formalize ihe omume na Lean 4 megide Mathlib. The output is a transcript, a set of rulings, a verdict, na ebe formalization e mere n'ihi, the Lean result.
2. Gịnị bụ ihenhọrọ ahụ na ọ bụghị
Ọrụ ahụ e mepụtara site na ngwe nke atọ AI models na ọ bụghị n'aka. Ọ bụghị iwu, ọgwụ, ego, injinịri ma ọ bụ ndụmọdụ ọrụ nke ụdị ọ bụla, na ọ dịghị mmekọrịta ọrụ e mepụtara site n'iji ọrụ a.
The referee ruling a criterion met is a statement about the evidence on record in that match. It is not a guarantee of correctness. AI models make mistakes, misread sources, and can fabricate citations despite instructions not to. You must independently verify anything you intend to rely on, particularly before publishing it, submitting it, or acting on it. This is a tool for pressure-testing work, not a substitute for qualified human review.
N'ihi na Lean formalization na-arụ ọrụ nke ọma, Lean kernel na-anabata ihe ngosipụta nke okwu ahụ e mepụtara, n'ebe ọha nke Mathlib na-eji ya n'oge ahụ. Ọ bụghị ya bụ na okwu ahụ bụ ntụgharị n'ụzọ ziri ezi nke ihe ịjụla, na ịhọrọ okwu n'ụzọ ziri ezi nke na-ekwughị ihe ịchọrọ bụ ụzọ kachasị n'ụzọ ziri ezi nke ihe ịhụnanya. Gụọ okwu n'ụzọ ziri ezi, ọ bụghị naanị nghọta.
Ihenhọrọ gị
I na-echekwa ikike nke n'ekwenyere na ị na-eziga na nke nke a na-eweta maka gị. I na-enye anyị naanị ikike ahụ ejiri rụọ ọrụ: iji rụọ ọrụ na ị na-eziga, gbanwee ya na ndị na-enye model ị họọrọ, na chekwa ihe a na-eme ka match ka ị wee nwee ike ịnaghachi ya.
Matches bụ nke onwe site na difọ́ọ̀ltụ̀. Ọ bụrụ na ị mara match nke ndị mmadụ, ọ ga-egosipụtara n'ebe ọbụla na njikọ ahụ ma ọ bụ na-egosipụta na anyị ndị mmadụ gallery. Enweghị ike ịdebata match nke nwere ihe ọbụla nke n'ime.
Enweghị ike ịnye data nkeonwe banyere ndị ọzọ, ihenhọrọ n'ime onwe gị ịnweghị ikike ịkekọrịta, ma ọ bụ ihenhọrọ nke ọha na eze.
4. Credits na mbipụta
Credit bụ nke a na-akwụ n'ihu ma a na-eji ya dịka matches na-arụ ọrụ. match ọbụla nwere ojiji nke ịhazie; ịga n'ihu na-ewepụ match n'ebe ahụ ka ọ na-aga n'ihu na-eji ya. Oji ndị ahụ enweghị ike ịgbanwe ma ọ bụ, ọbụla ebe achọrọ ya site na iwu, enweghị ike ịnabata mgbe a na-eji ya. Credit a na-ejighị ya nwere ike ịnabata mgbe achọrọ ya.
Ọ bụrụ na ịkpọnye kii nghọta gị, ị ga-akwụ ụgwọ onye na-enye gị n'ụzọ nkịtị nakwa anyị ga-ebipụtaghị ụgwọ ọbụla n'otu token. N'ebe ahụ, ọbụla n'ebe ahụ, ụgwọ n'imewe ga-abịa n'ime iji rụọ ọrụ paneelụ, ngwaọrụ na nchekwa.
Anyị nwere ike ịgbanwe ọnụahịa na nkwenye. Ngbanwe ndị ahụ anaghị adị na kredit eburula.
Oge ojiji
Enweghị ike iji ọrụ a mee ihe n'ime nke na-emebi ndị ọzọ, iji wepụ anyị n'ihe n'ime ma ọ bụ usoroiheomume, iji wepụ n'ime ihe n'ime ma ọ bụ n'ime usoroiheomume, ma ọ bụ iji ree n'ime na-enweghị nkwekọrịta. Nnweta-code-execution tool bụ maka ịhụ na ihe achọrọ; enweghị ike iji ya mee ihe n'ime usoroiheomume ọ bụla.
Nhazi
Anyị na-adabere na ndị na-enye móòdù nke atọ. Ndị na-enye móòdù na-akwụsị, na-agbanwe mòdù, nakwa na-ewepụ ha. A match nke a na-egbochi maka ihe ọbụla bụ n'okpuru nkwụsị na-aga n'ihu; anyị anaghị akwụ ụgwọ maka ọrụ nke a na-emeghị. Anyị anaghị akwado n'ịrụ ọrụ na-enweghị nkwụsị, na móòdù ị na-eji n'oge gara aga nwere ike ịbụ na-enweghị ike.
Nlekọta
N'ihi na zuru ezu n'ebe a na-enye ikike site na iwu, ọrụ a na-enye dị ka ọ bụ na-enweghị warranties nke ụdị ọ bụla. Anyị zuru ezu n'ihi na ọ bụla n'ihi na-akwụsị na-akwụsị na ego ị na-akwụ anyị n'ime ọnwa atọ tupu n'ihi na-akwụsị na-akwụsị. Anyị bụ na-enweghị n'ihi na n'ihi na n'ihi na n'ihi na n'ihi na n'ihi na n'ihi na n'ihi na n'ihi na n'ihi na n'ihi na n'ihi na n'ihi na n'ihi na n'ihi na n'ihi na n'ihi na n'ihi na n'ihi na n'ihi na n'ihi na n'ihi na n'ihi na n'ihi na n'ihi na n'ihi na n'ihi na n'ihi na n'ihi na n'ihi na n'ihi na n'ihi na n'ihi na n'ihi na n'ihi na n'ihi na n'ihi na n'ihi na n'ihi na n'ihi na n'ihi na n'ihi na n'ihi na n'ihi na n'ihi na n'ihi na n'ihi na n'ihi na n'ihi na n'ihi na n'ihi na n'ihi na n'ihi na n'ihi na n'ihi na n'ihi na n'ihi na n'ihi na n'ihi na n'ihi na n'ihi na n'ihi na n'ihi na n'ihi na n'ihi na n'ihi na n'ihi na n'ihi na n'ihi na n'ihi na n'ihi na n'ihi na n'ihi na n'ihi na n'ihi na n'ihi na n'ihi na n'ihi na n'ihi na n'ihi na n'ihi na n'ihi na n'ihi na n'ihi na n'ihi na n'ihi na n'ihi na n'ihi na n'ihi na n'ihi na n'ihi na n'ihi na n'ihi na n'ihi na n'ihi na n'ihi na n'ihi na n'ihi na n'ihi na n'ihi na n'ihi na n'ihi na n'ihi na n'ihi na n'ihi na n'ihi na n
Nkwụsị
I nwere ike igbochi akaụntụ gị mgbe ọbụla; anyị ga-ebuli ego na-ejighị ya. Anyị nwere ike igbochi akaụntụ ndị na-emebi iwu ndị a ma ọ bụ na-eweta ọrụ na nhụjuanya.
9. Ngbanwe, asụsụ na nrụnye
Anyị nwere ike ịgbanwe ọnọdụ ndị a; mgbanwe ndị dị mkpa ga-egosipụta na saịtị ahụ.
Ntụgharị nke ihuakwụkwọ a na-enye maka nchebe nakwa maka mmepe nke igwe. Ebe ntụgharị na nsụgharị na-adabere, nsụgharị na-adabere.
Ajụjụ: Kpọnye na anyị.