Finite Field / Math Lab

Jenga ushahidi wa usahihi, si matokeo ya haraka pekee.

Math Lab ni mahali tunapoonyesha jinsi tunavyoshughulikia uundaji wa modeli za kihisabati, uthibitishaji wa teorema, uthibitishaji rasmi, uwezo wa kurudiwa na utekelezaji unaoaminika bila kuzidisha ushahidi.

Tazama maeneo ya utafiti Fungua ukurasa wa NPA

Miradi ya umma: NPA / STD / MATHLIB
Lugha kuu: Rust
Muhtasari wa NPA: v0.1.1

Ukaguzi wa uthibitisho / mtazamo wa dhana Kusoma tu

01 baiti sanifu / umbizo SAWA

02 hashi_ya_cheti SAWA

03 ukaguzi wa uthibitisho tegemezi SAWA

04 hukumu bila chanzo SAWA

Mpaka wa uaminifu unaonekana Ukurasa huu haudai kuwa NPA ni mbadala wa vitendo wa Lean au Rocq, na uigaji wa kivinjari hauendeshi NPA.

Kanuni ya maabara

Chapisha si matokeo pekee, bali pia mpaka wa ukaguzi.

Hitimisho kama “ilifanya kazi,” “ilikuwa haraka,” au “imethibitishwa” halitoshi. Tunaonyesha maingizo, dhana, sehemu zinazoaminika, vielelezo vinavyoweza kukaguliwa kwa uhuru na masuala ambayo hayajatatuliwa kando kando.

01 / Mpaka

Weka msingi unaoaminika uwe mdogo

Usiweke vizalishaji changamano au AI katikati ya uaminifu. Fanya upande mdogo wa ukaguzi uwe wazi.

02 / Ushahidi

Fanya ushahidi uwe kielelezo

Acha vyeti, hashi, orodha za dhana, masharti ya kulinganisha na kumbukumbu katika umbo ambalo wengine wanaweza kukagua.

03 / Rudia

Buni kwa uwezo wa kurudiwa

Funga msururu wa zana, data ya ingizo, amri za utekelezaji na vigezo ili matokeo yaweze kukaguliwa tena.

04 / Uwazi

Usizidishe hali ya utafiti

Onyesha mbinu za vitendo, majaribio na utafiti kando kando. Weka mipaka karibu na matokeo.

MAPITIO YA MBINU

Kategoria ya mbinu ya huduma ambayo bado inahitaji wigo, wajibu, ushahidi wa mteja na idhini kabla ya kuelezwa kuwa iko tayari kwa mradi.

MAJARIBIO

Utekelezaji unaofanya kazi upo, lakini ukubwa, upatanifu, utendaji au mabadiliko ya vipimo bado yanawezekana. Toleo na hatua za kurudia zinahitajika.

UTAFITI

Usanifu, tathmini, uthibitisho au utekelezaji unaendelea. Hii haimaanishi kupatikana kibiashara au kukamilika.

Jalada la utafiti

Tazama utafiti kwa ukomavu na vielelezo.

Kila kadi inaonyesha ukomavu, vielelezo, hali ya sasa na uthibitishaji unaofuata. Utafutaji na vichujio hutumia hali ya upande wa kivinjari pekee.

8 zinaonyeshwa

MAJARIBIO HURIA

Nano Proof Auditor

Msururu wa zana za uthibitisho unaotanguliza vyeti

Msururu wa zana za utafiti unaoweka vyeti sanifu vya uthibitisho na msingi mdogo wa ukaguzi katikati ya mapitio ya uthibitisho tegemezi.

Vielelezo: chanzo / ubainishaji / violezo vya CI
Sasa: picha ya umma ya v0.1.1
Uthibitishaji unaofuata: vifurushi vya nje vya teorema na ukaguzi huru

Fungua maelezo ya NPA

MAJARIBIO HURIA

Maktaba Sanifu ya NPA

Logic / Nat / List / Algebra

Hazina ya kawaida ya vifurushi vya teorema kwa misingi ya NPA inayoweza kutumika tena.

Vielelezo: chanzo / vifurushi vya uthibitisho
Sasa: hazina ya umma iliyogawanywa
Uthibitishaji unaofuata: upeo wa kifurushi na upatanifu

GitHub

UTAFITI HURIA

Maktaba ya Hisabati ya NPA

Maktaba rasmi ya hisabati

Mwelekeo wa maktaba kwa kuhifadhi teorema za hisabati kama vifurushi vya uthibitisho vinavyoweza kukaguliwa kwa uhuru.

Vielelezo: chanzo / vifurushi vya uthibitisho
Sasa: hazina ya umma inayoendelezwa
Uthibitishaji unaofuata: muundo wa maktaba na ukaguzi wa utegemezi

GitHub

MAPITIO YA MBINU MBINU

Modeli za upangaji zenye vikwazo

Ratiba / Njia / Ugawaji

Mbinu ya kutenganisha vikwazo visivyovunjika na vipimo vya tathmini katika zamu, ziara, njia, uzalishaji na kazi za ugawaji.

Vielelezo: modeli / kielelezo / ripoti ya maelezo
Sasa: mbinu ya huduma; dai la umma limewekewa mipaka kwa mapitio ya mbinu
Uthibitishaji unaofuata: ushahidi wa mteja na idhini ya upeo

Tazama mfano wa awali

UTAFITI UPIMAJI

Tathmini ya kisuluhishi inayoweza kurudiwa

Vipimo na ushahidi

Mpango wa kufunga seti za mifano, vifaa, mipaka ya muda, mbegu nasibu na kumbukumbu ghafi kabla ya kutoa madai ya utendaji.

Vielelezo: sajili ya vipimo / kumbukumbu ghafi / ripoti
Sasa: muundo wa programu ya utafiti
Uthibitishaji unaofuata: mkusanyo wa kwanza wa umma wa vipimo

Tazama mbinu

UTAFITI MBINU RASMI

Uthibitishaji wa mantiki muhimu ya biashara

Kanuni zisizobadilika kwa mifumo ya biashara

Utafiti wa kutenganisha ada, ruhusa, akiba na mabadiliko ya hali kuwa vipimo na kanuni zisizobadilika.

Vielelezo: ubainishaji / kanuni zisizobadilika / ripoti ya jaribio au uthibitisho
Sasa: utafiti wa upeo
Uthibitishaji unaofuata: chagua kisa kimoja kilichowekewa mipaka na kinachofanana na uzalishaji

Tazama usanifu wa usalama

MAJARIBIO UHANDISI

Vipengele vidogo vinavyoaminika katika Rust

Vipengele vidogo vinavyoaminika

Kazi ya utekelezaji inayoweka vipande muhimu vya uaminifu kama vikaguzi na hashi kuwa vidogo vya kutosha kukaguliwa.

Vielelezo: kiini cha NPA / crate ya cheti / kikaguzi cha marejeo
Sasa: utekelezaji wa umma katika NPA
Uthibitishaji unaofuata: upatanifu wa kikaguzi huru

Tazama chanzo

UTAFITI AI × UTHIBITISHO

Usaidizi wa AI na ukaguzi huru

Zalisha kwa uhuru, thibitisha kwa ukali

Mwelekeo wa utafiti unaoweka AI kwenye uzalishaji wa wagombea huku ushahidi wa mwisho ukikaguliwa kwa uhuru.

Vielelezo: jenereta ya mgombea / cheti / ripoti ya kikaguzi
Sasa: mwelekeo wa utafiti unaolingana na modeli ya uaminifu ya NPA
Uthibitishaji unaofuata: mtiririko wa uandishi uliopimwa

Tazama mpaka wa uaminifu

Hakuna eneo la utafiti linalolingana lililopatikana.

Jaribu neno lingine au rudisha kichujio cha ukomavu kuwa vyote.

Nano Proof Auditor

Tenganisha uzalishaji wa uthibitisho na kile tunachoamini.

NPA ni msururu wa zana za uthibitisho unaotanguliza vyeti kwa uthibitisho tegemezi. Sehemu za mbele, mbinu, utafutaji wa teorema, programu-jalizi, AI, faili chanzo na hali ya CI zinaweza kusaidia kuunda wagombea, lakini si ushahidi wa uthibitisho unaoaminika.

MAJARIBIOHURIAAPACHE-2.0

Muhtasari wa sasa

v0.1.1

Taarifa za umma zilikaguliwa tarehe 2026-06-21.

Kiini kikuu

Rust

Kithibitishaji cha Rust na kiini ni sehemu ya upande wa ukaguzi.

Kielelezo cha ukaguzi

.npcert

Baiti sanifu za cheti ndizo kitu cha kukaguliwa.

Sehemu ya kukagua tena

mapitio ya mikono

Hali ya hazina na mwonekano wa kifurushi lazima vikaguliwe kabla ya kuchapishwa.

Kichunguzi cha mpaka wa uaminifu

Bofya ili kuona kinachoaminika na kisichoaminika.

Bofya kila nodi ili kukagua inachofanya, inachozalisha na ukaguzi gani bado unahitajika.

HAIAMINIKI

IMEKAGULIWA

Mpaka muhimu

NPA kwa sasa si mbadala wa vitendo wa Lean au Rocq. Ukurasa huu unaeleza usanifu wa utafiti unaozingatia vyeti na hauhakikishi mifumo ya kibiashara isiyo na hitilafu wala utatuzi wa teorema kiotomatiki.

Ukaguzi wa cheti / uigaji wa maelezo

Jione mtiririko wa ukaguzi wa vyeti.

Mwingiliano wa kivinjari unaeleza mtiririko wa ukaguzi. Hauendeshi NPA, Rust, WASM wala vyeti halisi vya uthibitisho.

Mfano wa CLI

npa package verify-certs --root . --checker reference --json

NPA / mkondo wa ukaguzi TAYARI

01 Soma chetibaiti sanifu / umbizo SUBIRI
02 Kagua hashi ya chetihashi_ya_cheti SUBIRI
03 Kagua kwa kiiniukaguzi wa uthibitisho tegemezi SUBIRI
04 Kagua tena kwa kikaguzi cha rejeahukumu bila chanzo SUBIRI
05 Linganisha ripoti ya axiomshashi ya ripoti ya axioms SUBIRI

Hukumu

Maelezo bado hayajaendeshwa.

Endesha maelezo ili kuona hatua kwa mpangilio.

Mfumo ikolojia wa uthibitisho

Fafanua majukumu badala ya kupanga zana kwa ubora.

Lean na Rocq ni mifumo ikolojia iliyokomaa ya wasaidizi wa uthibitishaji. NPA inaonyeshwa hapa kama mradi wa utafiti na utekelezaji unaozingatia vyeti, si kama orodha ya mbadala bora.

Kipengee	Lean	Rocq	NPA
Nafasi	Lugha huria ya programu na msaidizi wa uthibitishaji.	Kithibitishaji shirikishi cha teorema chenye historia ndefu ya utafiti.	Hazina ya utafiti na utekelezaji kwa ukaguzi unaoanza na vyeti.
Matumizi ya kawaida	Hisabati, uthibitishaji wa programu na upangaji programu.	Hisabati, vipimo, uthibitishaji wa programu na uchimbaji.	Utafiti kuhusu vyeti vya uthibitisho na ukaguzi huru.
Msisitizo	Upanuzi, maktaba na uthibitishaji shirikishi.	Uwezo wa kueleza, mbinu zilizokomaa na maktaba.	Msingi mdogo unaoaminiwa na vyeti sanifu.
Jinsi ukurasa huu unavyoitazama	Rejea ya kujifunza, kulinganisha na kuingiliana.	Rejea ya kujifunza, kulinganisha na mbinu za uundaji rasmi.	Mradi wa utafiti wa Finite Field.
Mpaka	Maarifa ya kitaalamu bado yanahitajika.	Maarifa ya kitaalamu bado yanahitajika.	Haikusudiwi kuwa mbadala wa vitendo wa Lean au Rocq kwa sasa.

Tovuti rasmi ya Lean Tovuti rasmi ya Rocq Prover NPA GitHub

Mbinu ya utafiti

Geuza “ilifanya kazi” kuwa utaratibu wa ukaguzi unaoweza kurudiwa.

Matokeo huwa imara zaidi mtu mwingine akiweza kuyaendesha tena, kuyakagua na kuyakataa chini ya masharti yale yale.

Swali

Fafanua kinachopaswa kukaguliwa: utendaji, usahihi, upatanifu au wigo.

Dhana

Andika dhana, yaliyoondolewa, axioms, mapengo ya data na upendeleo kabla ya tathmini.

Kielelezo

Hifadhi chanzo, vyeti, maingizo, kumbukumbu za utekelezaji na hashi.

Ukaguzi huru

Kagua matokeo kupitia njia tofauti na upande wa kuzalisha.

Kipimo cha kulinganisha

Funga vifaa, matoleo, mipaka ya muda, seti za mifano na mbegu nasibu.

Mipaka

Chapisha kushindwa, kesi zisizosaidiwa, mipaka ya utendaji na uthibitishaji unaofuata.

Kijenzi cha uwezo wa kurudiwa

Kagua kinachokosekana bado katika uchapishaji wa utafiti.

Orodha ya ukaguzi huchakatwa kwenye kivinjari pekee. Si alama ya uidhinishaji.

Utayari

Swali la utafiti na sharti la mafanikioKinachohesabika kama mafanikio au kushindwa. Zana na utegemezi vilivyofungwaMatoleo, faili za kufunga, vifaa na mazingira. Data ya ingizo au mchakato wa kuzalishaKuficha utambulisho, leseni, chanzo na hashi. Mlolongo wa amri za kuendesha tenaKutoka uanzishaji hadi uzalishaji wa matokeo. Vielelezo vinavyokaguliwa na kumbukumbu ghafiVyeti, ripoti, kumbukumbu na hashi. Mipaka, kushindwa na maswali waziKesi zisizosaidiwa na masuala ambayo hayajatatuliwa.

Hatua inayofuata

Fafanua kwanza swali la utafiti na sharti la mafanikio.

Kabla ya kuamua miundo ya vielelezo, thibitisha kitakacholinganishwa au kukaguliwa.

Vielelezo vya umma

Fuatilia vielelezo vya umma kutoka lango moja.

Ukurasa huepuka miito ya GitHub API wakati wa utekelezaji. Hali ya hazina ni muhtasari uliokaguliwa ambao lazima uthibitishwe kabla ya kuchapishwa.

4 vielelezo

finitefield-org

npa

msururu wa zana za uthibitisho unaotanguliza vyeti

Rust / OCamlApache-2.0Majaribio

KAGUA kifurushi verify-certs

finitefield-org

npa-std

kifurushi sanifu cha teorema

UthibitishoKifurushiMajaribio

JUKUMU Std.Logic / Nat / List

finitefield-org

npa-mathlib

maktaba rasmi ya hisabati

HisabatiUthibitishoUtafiti

JUKUMU vifurushi rasmi vya teorema

GitHub

finitefield-org

kielezo cha hazina za umma

ShirikaHuria

KIELEZO hazina zote za umma

Hakuna kielelezo cha umma kinacholingana na utafutaji.

Sera ya uchapishaji

Hazina za umma, madokezo ya utafiti na vipimo vinapaswa kubeba tarehe ya ukaguzi, ukomavu, hatua za kurudia na mipaka inayojulikana. Idadi ya nyota na mabadiliko yaliyowekwa haionyeshwi kama ishara ya ubora wa utafiti.

Kutoka maabara hadi uendeshaji

Leta nidhamu ya utafiti katika usanifu wa mifumo ya biashara.

Si kila mfumo wa mteja unahitaji uthibitishaji wa teorema. Kilicho muhimu kuhamishwa ni kuamua nini kiaminike, kilinganishwe, kikaguliwe, kisahihishwe na kiidhinishwe na watu.

Mazoezi ya maabara

Mipaka ya uaminifu

Tenganisha uzalishaji wa wagombea, hesabu na ukaguzi wa mwisho badala ya kuamini kila safu kwa kiwango sawa.

Ushahidi

Hifadhi maingizo, matokeo, vyeti, hashi na kumbukumbu kama vielelezo vinavyoweza kukaguliwa.

Uwezo wa kurudiwa

Funga data, matoleo, amri na vigezo vya tathmini kabla ya kulinganisha matokeo.

Mipaka

Chapisha vikwazo, kesi zilizoshindwa na hoja ambazo hazijatatuliwa kwa uzito sawa na matokeo.

Mfumo wa mteja

Mamlaka na wajibu

Fafanua nani huingiza, nani hukagua, nani hubatilisha na nani huthibitisha matokeo.

Sababu za uamuzi

Onyesha vikwazo, alama za tathmini, wagombea waliokataliwa na hoja ambazo hazijatatuliwa.

Uwezo wa kukaguliwa

Hifadhi mabadiliko ya masharti, raundi za hesabu na historia ya idhini ya mwisho.

Uamuzi wa binadamu

Fanya matokeo ya otomatiki yaweze kusahihishwa, kukataliwa na kuelezwa kwa waendeshaji.

01 Zamu na upangaji wa wafanyakazi

Onyesha ukiukaji wa sheria na kutimizwa kwa mapendeleo kando kando.

02 Upangaji wa njia za magari

Weka sababu za njia, uwezo, madirisha ya muda na hali zisizo za kawaida zikiwa wazi.

03 Upangaji wa ratiba za uzalishaji

Eleza kazi ambazo hazijapangwa, vizuizi vya uwezo na maamuzi ya kubadilishana katika maandalizi.

04 Ulinganishi wa ugawaji

Onyesha sababu za wagombea na mbadala kabla ya idhini.

Madokezo ya utafiti

Weka historia ya masasisho na ushahidi visomeke.

Si kila kadi ni makala iliyochapishwa. Madokezo yanayoandaliwa hayaitwi kazi iliyochapishwa hadi yapate tarehe, vyanzo na hatua za kurudia.

NPA / Sasa2026.06.21

Kwa nini kuweka vyeti katikati

Kwa nini ushahidi wa mwisho unapaswa kuwa cheti sanifu kinachokaguliwa kwa njia ndogo huru.

Tazama hazina ya umma

Dokezo la usanifu / limepangwaInaandaliwa

Kufanya matokeo ya uboreshaji yaweze kuelezeka

Dokezo la usanifu kuhusu kuonyesha malengo, vikwazo visivyovunjika, mapendeleo laini na ugawaji ambao haujatatuliwa kwenye kiolesura.

Tazama demo zinazohusiana

Kipimo cha kulinganisha / kimepangwaInaandaliwa

Masharti ya kulinganisha kisuluhishi kwa haki

Dokezo lililopangwa kuhusu seti za mifano, mipaka ya muda, mapengo ya ubora, mbegu nasibu na vifaa.

Tazama vigezo vya uchapishaji

Vipengee vya “Inaandaliwa” si makala zilizochapishwa. Baada ya kuchapishwa, kila dokezo hupata tarehe, chanzo, mwandishi, njia ya kurudia na mipaka inayojulikana.

Maswali ya mara kwa mara

Mipaka ya utafiti, zana za uthibitishaji na matumizi ya biashara.

Hoja hizi huwekwa wazi ili kurasa za utafiti zisichanganywe na dhamana za uzalishaji.

Soma kuhusu kampuni

01 Je, Math Lab ni huduma ya uundaji kwa mkataba?

Hapana. Ni mahali pa kuchapisha msimamo wa utafiti na vielelezo. Katika mazungumzo na wateja, tunatenganisha mbinu zinazoweza kutumika, mbinu zinazohitaji uthibitishaji zaidi na mada zilizo katika hatua ya utafiti.

02 Je, NPA inaweza kuchukua nafasi ya Lean au Rocq?

Hapana. NPA ya sasa si mbadala wa vitendo wa Lean au Rocq. Ni mradi wa utafiti na utekelezaji kuhusu vyeti, ukaguzi huru na msingi mdogo unaoaminiwa.

03 Je, mnaamini uthibitisho uliotengenezwa na AI ulivyo?

Hapana. AI, utafutaji na mbinu husaidia kuunda wagombea. Tunazingatia kama cheti cha mwisho kinakubaliwa na kikaguzi kilicho huru kutoka njia hizo za kuzalisha.

04 Je, uthibitishaji rasmi huondoa hitilafu zote?

Hapana. Mbinu rasmi hukagua sifa maalum dhidi ya maelezo yaliyo wazi. Maelezo yasiyo sahihi, msimbo nje ya wigo, uendeshaji na huduma za nje bado zinahitaji mapitio tofauti.

05 Je, hii inahusiana na kazi ya mifumo ya biashara?

Ndiyo. Kwa kawaida tunatumia nidhamu hii hatua kwa hatua: vikwazo, sababu za matokeo, historia ya hesabu, mipaka ya ruhusa na ukaguzi wa mantiki muhimu ya biashara.

Jadili tatizo

Unaweza kujadili kazi inayopaswa kutatuliwa, si mada ya utafiti pekee.

Anza na lahajedwali la sasa, sheria na sehemu ambazo maamuzi husahihishwa na watu. Tunaweza kupanga kama uundaji wa modeli ya kihisabati, otomatiki ya sheria au mfano wa awali ndio uanze.

Kagua changamoto ya biashara Tazama mfano wa awali

Muhtasari wa chanzo / 2026-06-21

Madai kuhusu NPA yanategemea muhtasari wa hazina ya finitefield-org/npa. Nafasi ya Lean na Rocq inategemea tovuti zao rasmi. Hali ya hazina, tagi za karibuni na maneno ya mapitio ya mbinu yalikaguliwa tarehe 2026-06-28.