Javno stanje
Istraživački i implementacijski repozitorij
GitHub repozitorij je javan, ali ova stranica opisuje istraživački i implementacijski repozitorij, ne uvedenu uslugu.
Natrag na Math Lab
NPA / Provjera dokaza s certifikatom u središtu
NPA: prikažite granicu dokaznog materijala prije nego što povjerujete rezultatu.
Ova stranica rekonstruira NPA odjeljak iz Math Laba kao samostalnu stranicu dokaza: javno stanje, model povjerenja, tijek dokaza, registar tvrdnji, repozitorije, izvore i izričitu formulaciju da nije zamjena.
- Javno stanje
- Istraživački repozitorij
- Prikazano kao istraživanje i implementacija, ne kao usluga proizvodnog jamstva.
- Javna ponovna provjera
- 2026-07-02 / NPA v0.2.0
- Provjerene najnovije git oznake: npa v0.2.0, npa-std v0.1.0, npa-mathlib v0.1.30.
- Licenca
- Apache-2.0
- Licenca Apache-2.0 provjerena je za npa, npa-std i npa-mathlib 2026-07-02.
Javno ponovno očitanje: 2026-07-02. Najnovija git oznaka NPA repozitorija je v0.2.0; npa-std je v0.1.0; npa-mathlib je v0.1.30. Fiksirane verzije iz README datoteka paketa prikazane su kao kontekst specifičan za repozitorij i ne spajaju se u jednu tvrdnju o NPA verziji.
Javno stanje
Navedite što je javno, što je dokaz i kada je ponovno provjereno.
Ova stranica čini osnovu stranice vidljivom: lokalnu snimku istine, javni izvor repozitorija i datum završnog očitanja prije objave.
Javna ponovna provjera
2026-07-02
Očitanje javnog izvora dovršeno je 2026-07-02. Izvorna rekonstrukcija i dalje koristi lokalnu snimku istine od 2026-06-21.
Dokazi
Certifikati i hashovi
Snimka izvora bilježi kanonski .npcert, certificate_hash, export_hash, axiom_report_hash i presude provjerivača.
Licenca
Apache-2.0 licenca provjerena
Apache-2.0 provjeren je za npa, npa-std i npa-mathlib kroz javne LICENSE metapodatke 2026-07-02.
Granica
NPA nije praktična zamjena za Lean ili Rocq. Distribuirana simulacija pregleda u pregledniku ne pokreće NPA. Javne oznake, licenca i vidljivost repozitorija provjereni su 2026-07-02 za završno očitanje prije objave.
Granica povjerenja
Preko granice dokaza premjestite samo kanonski certifikat.
Granica nije u tome koji alat izgleda sofisticirano. Radi se o tome kojem je artefaktu dopušteno postati dokaz nakon neovisne provjere.
Parser, elaborator, taktike, automatizacija, pretraživanje teorema, dodaci, AI sustavi, izvorne datoteke, datoteke ponavljanja, indeksi teorema, planovi objave, CI status, stranice izdanja i metapodaci registra ostaju na nepouzdanoj strani kandidata.
Tijek dokaza / objašnjavajuća simulacija
Prikažite točan tijek od bajtova certifikata do dokaza provjere.
Simulacija u pregledniku ne pokreće NPA, Rust, WASM ni stvarne certifikate dokaza. Vizualizira redoslijed provjere bez izvornog koda koji stvarni artefakti moraju zadovoljiti.
CLI put dokaza
npa package verify-certs --root . --checker reference --json
NPA / revizijski trag
SPREMNO
- 01 Format certifikatakanonski .npcert bajtovi / certifikat koji se može parsirati / provjera formata ČEKA
- 02 Hash certifikatabajtovi certifikata / certificate_hash / deterministički sažetak ČEKA
- 03 Presuda kernelacertifikat / prihvati ili odbij / izvješće Rust provjerivača ČEKA
- 04 Referentni provjerivačcertifikat fiksiran hashom / neovisno prihvaćanje ili odbijanje / izvješće provjerivača bez izvornog koda ČEKA
- 05 Izvješće o aksiomimaprovjereni paket / axiom_report_hash / inventar pretpostavki ČEKA
Presuda
Objašnjavajući tijek još nije pokrenut.Pokrenite objašnjenje kako biste redom označili put provjere bez izvornog koda.
Registar tvrdnji
Odvojite dokaze, vremenski osjetljive činjenice i tvrdnje o granici.
Stranica se ne oslanja na neodređen istraživački tekst. Svaka javna izjava vezana je uz lokalnu snimku istine, izvor i radnju objave.
| Tvrdnja | Javna formulacija | Stanje | Izvor | Radnja objave |
|---|---|---|---|---|
| CL-001 | NPA stavlja certifikat u središte: granica koja se može revidirati jest kanonski .npcert artefakt i put provjere oko njega. | Provjerena javna tvrdnja | S01 / 2026-07-02 | Pregledati kada se README promijeni. |
| CL-002 | Javna ponovna provjera od 2026-07-02 pronašla je najnoviju git oznaku NPA repozitorija na v0.2.0. README datoteke povezanih paketa i dalje prikazuju pinove specifične za repozitorij, pa formulacija verzije ostaje ograničena na pojedini repozitorij. | Provjereno javno očitanje | S01 / S02 / 2026-07-02 | Formulaciju oznaka zadržati u opsegu repozitorija. |
| CL-003 | Lokalna snimka istine bilježi fiksiranu verziju alatnog lanca Rust 1.95.0; ne koristi se kao marketinška tvrdnja. | Provjereno, vremenski osjetljivo | S01 / 2026-07-02 | Ponovno provjeriti ako se verzija alatnog lanca prikazuje javno. |
| CL-004 | NPA nije praktična zamjena za Lean ili Rocq. Ta granica mora ostati vidljiva uz svaku usporedbu. | Provjerena tvrdnja o granici | S01 / S03 / S05 / 2026-07-02 | Zadržati napomenu o ograničenju. |
| CL-005 | npa-std i npa-mathlib zasebni su javni repozitoriji paketa teorema u organizaciji finitefield-org. | Provjerena javna tvrdnja | S01 / S02 / 2026-07-02 | Ponovno provjeriti vidljivost repozitorija ako se objava odgodi ili se repozitoriji promijene. |
| CL-006 | Repozitoriji npa, npa-std i npa-mathlib svaki prikazuju licencu Apache-2.0 kroz javne LICENSE metapodatke. | Provjerena javna tvrdnja | S01 / S02 / 2026-07-02 | Ponovno provjeriti LICENSE pri velikom izdanju. |
Repozitoriji i licence
Kod, repozitorije paketa i vidljivost organizacije držite izričitima.
Poveznice na repozitorije upućuju na javne izvore, ali nisu jamstvo da je trenutačna stranica sinkronizirana s najnovijim stanjem GitHuba.
4 repozitorija prikazano
finitefield-org
npa
Alatni lanac za pomoć pri dokazima i verifikaciju s certifikatom u središtu.
- Licenca
- Apache-2.0 provjerena je iz LICENSE datoteke 2026-07-02.
- Provjera
- Najnovija git oznaka: v0.2.0. Najnovije GitHub izdanje nije objavljeno. Trenutačna README referenca alatnog lanca: NPA_GIT_TAG=v0.2.0.
eksperimentalnoRust / OCamlcertifikat u središtu
Otvori repozitorij
finitefield-org
npa-std
Repozitorij standardnog paketa teorema za NPA izvore dokaza.
- Licenca
- Apache-2.0 provjerena je iz LICENSE datoteke 2026-07-02.
- Provjera
- Najnovija git oznaka i GitHub izdanje: v0.1.0. Verzija metapodataka README paketa: 0.1.0; fiksirana oznaka alatnog lanca paketa: NPA_GIT_TAG=v0.1.1.
eksperimentalnopaket teoremaizvor dokaza
Otvori repozitorij
finitefield-org
npa-mathlib
Istraživački repozitorij biblioteke formalne matematike.
- Licenca
- Apache-2.0 provjerena je iz LICENSE datoteke 2026-07-02.
- Provjera
- Najnovija git oznaka: v0.1.30. Najnovije GitHub izdanje: v0.1.9. Verzija metapodataka README paketa: 0.2.1; fiksirana oznaka alatnog lanca paketa: NPA_GIT_TAG=v0.1.1.
istraživanjeformalna matematikabiblioteka
Otvori repozitorij
finitefield-org
Finite Field GitHub organizacija
Javna snimka organizacije za Lab obitelj repozitorija.
- Licenca
- Primjenjuju se licence pojedinih repozitorija
- Provjera
- npa, npa-std i npa-mathlib javni su prema GitHub API očitanju od 2026-07-02.
javni indekssnimka vidljivostiizvor
Otvori organizaciju
Nijedan repozitorij ne odgovara trenutačnom pretraživanju.
GitHub repozitoriji izvor su za javni status koda. Licenca, trenutačne oznake, javna vidljivost i formulacije izdanja provjereni su 2026-07-02 kao završno očitanje M10-T14.
Zaštitna usporedba ekosustava dokaza
Razjasnite uloge prije usporedbe alata za dokaze.
Ovo je tablica uloga, a ne rangiranje. Lean i Rocq ostaju referentni ekosustavi pomoćnika za dokaze; NPA je prikazan kao istraživački i implementacijski rad usmjeren na certifikate.
| Stavka | Lean | Rocq | NPA |
|---|---|---|---|
| Položaj | Programski jezik otvorenog koda i pomoćnik za dokaze. | Interaktivni dokazivač teorema s dugom istraživačkom poviješću. | Repozitorij za istraživanje i implementaciju provjere usmjerene na certifikate. |
| Tipična uporaba | Matematika, verifikacija softvera i programiranje. | Matematika, specifikacije, verifikacija programa i ekstrakcija. | Istraživanje certifikata dokaza, neovisne provjere i male pouzdane baze. |
| Granica dokaza | Vlastiti pouzdani kernel i ekosustav definiraju granicu provjere. | Vlastiti kernel i provjereni razvojni rad definiraju granicu provjere. | Kanonski .npcert artefakt prelazi iz generiranja u provjeru. |
| Kako ova stranica to prikazuje | Referenca za učenje, usporedbu i interoperabilnost. | Referenca za učenje, usporedbu i metode formalizacije. | Istraživački projekt Finite Fielda, ne obećanje proizvoda. |
| Granica | I dalje je potrebno stručno znanje. | I dalje je potrebno stručno znanje. | NPA trenutačno nije praktična zamjena za Lean ili Rocq. |
Izvori
Objavite mapu izvora uz interpretaciju.
Izvori su prikazani kako bi čitatelj mogao razlikovati tvrdnje koje dolaze iz javnih repozitorija, službenih stranica alata za dokaze i konteksta tvrtke.
S01
finitefield-org/npa
Primarni izvor za svrhu NPA-a, model povjerenja, formulaciju trenutačne oznake repozitorija v0.2.0, naredbe, raspored repozitorija i licencu.
Otvori izvor S02Finite Field GitHub organizacija
Primarni izvor za javnu vidljivost repozitorija, najnovije git oznake, stranice izdanja i snimku Lab obitelji repozitorija provjerenu 2026-07-02.
Otvori izvor S03Službena stranica Leana
Primarni izvor za javno pozicioniranje Leana, provjeren 2026-07-02.
Otvori izvor S04Referenca jezika Lean
Primarni izvor za kontekst teorije zavisnih tipova i referencu kernela, provjeren 2026-07-02.
Otvori izvor S05Službena stranica Rocq Provera
Primarni izvor za javno pozicioniranje Rocqa, provjeren 2026-07-02.
Otvori izvor S06FINITE FIELD stranica tvrtke
Izvor tvrtke za brend Finite Field i poslovni kontekst.
Otvori izvorFAQ
Stanje NPA-a i granice verifikacije.
Odgovori naglašavaju granicu povjerenja prije nego što čitatelji istraživačku stranicu zamijene za uvedenu uslugu pomoćnika za dokaze.
Pročitajte o tvrtki01 Je li ova stranica jamstvo proizvoda?
Ne. NPA je ovdje prikazan kao istraživački i implementacijski repozitorij.
02 Može li NPA zamijeniti Lean ili Rocq?
Ne. NPA nije praktična zamjena za Lean ili Rocq.
03 Pokreće li stranica stvarnu NPA verifikaciju?
Ne. Simulacija u pregledniku ne pokreće NPA, Rust, WASM ni stvarne certifikate dokaza.
04 Što se ovdje računa kao dokaz?
Certifikat, deterministički hashovi, rezultat Rust kernela/provjerivača, rezultat referentnog provjerivača bez izvornog koda i izvješće o aksiomima čine dokaze na strani provjere.
05 Koje činjenice treba ponovno provjeriti?
Trenutačna javna verzija, vidljivost repozitorija, fiksirane oznake alatnog lanca, tekst licence i formulacije izvora ponovno su provjereni 2026-07-02.
Od discipline dokaza do operacija
Istu disciplinu dokaza upotrijebite kada poslovna odluka mora biti pouzdana.
Za poslovne sustave korisna pouka nije dodati dokazivanje teorema posvuda. Korisno je odlučiti što treba generirati, provjeriti, zapisati, ispraviti i odobriti ljudima.