Javni status
Istraživački i implementacioni repozitorijum
GitHub repozitorijum je javan, ali ova stranica opisuje istraživački i implementacioni repozitorijum, ne uvedenu uslugu.
Nazad na Math Lab
NPA / Provera dokaza sa sertifikatom na prvom mestu
NPA: pokažite granicu dokaznog materijala pre nego što se rezultatu poveruje.
Ova stranica rekonstruše NPA odeljak iz Math Laba kao samostalnu stranicu dokaza: javni status, model poverenja, dokazni tok, registar tvrdnji, repozitorijumi, izvori i izričit tekst da NPA nije zamena.
- Javno stanje
- Istraživački repozitorijum
- Prikazano kao istraživanje i implementacija, ne kao proizvodna usluga garancije.
- Javna ponovna provera
- 2026-07-02 / NPA v0.2.0
- Proverene 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 proverena je za npa, npa-std i npa-mathlib 2026-07-02.
Javna ponovna provera: 2026-07-02. Najnovija git oznaka NPA repozitorijuma je v0.2.0; npa-std je v0.1.0; npa-mathlib je v0.1.30. README pinovi paketa prikazani su kao kontekst specifičan za repozitorijum i ne svode se na jednu tvrdnju o NPA verziji.
Javni status
Navedite šta je javno, šta je dokaz i kada je ponovo provereno.
Ova stranica čini osnovu stranice vidljivom: lokalni snimak istine, javni izvor repozitorijuma i datum završnog očitavanja pre objave.
Javna ponovna provera
2026-07-02
Očitavanje javnih izvora završeno je 2026-07-02. Izvorna rekonstrukcija i dalje koristi lokalni snimak istine od 2026-06-21.
Dokazi
Sertifikati i hashovi
Snimak izvora beleži kanonski .npcert, certificate_hash, export_hash, axiom_report_hash i presude proverivača.
Licenca
Apache-2.0 licenca proverena
Apache-2.0 licenca proverena je za npa, npa-std i npa-mathlib kroz javne LICENSE metapodatke 2026-07-02.
Granica
NPA nije praktična zamena za Lean ili Rocq. Distribuirana simulacija pregleda u pregledaču ne pokreće sam NPA. Javne oznake, licenca i vidljivost repozitorijuma provereni su 2026-07-02 za završno očitavanje pre objave.
Granica poverenja
Preko granice dokaza premestite samo kanonski sertifikat.
Granica nije u tome koji alat izgleda sofisticirano. Radi se o tome kojem artefaktu je dozvoljeno da postane dokaz nakon nezavisne provere.
Parser, elaborator, taktike, automatizacija, pretraga teorema, dodaci, AI sistemi, izvorni fajlovi, fajlovi ponavljanja, indeksi teorema, planovi objave, CI status, stranice izdanja i metapodaci registra ostaju na nepouzdanoj strani kandidata.
Dokazni tok / objašnjavajuća simulacija
Prikažite tačan tok od bajtova sertifikata do dokaznog materijala provere.
Simulacija u pregledaču ne pokreće sam NPA, Rust, WASM niti stvarne dokazne sertifikate. Ona prikazuje redosled provere bez izvora koji stvarni artefakti moraju zadovoljiti.
Put dokaza iz CLI-ja
npa package verify-certs --root . --checker reference --json
NPA / revizorski trag
SPREMNO
- 01 Format sertifikatakanonski .npcert bajtovi / sertifikat koji se može parsirati / provera formata ČEKA
- 02 Hash sertifikatabajtovi sertifikata / certificate_hash / deterministički sažetak ČEKA
- 03 Presuda kernelasertifikat / prihvati ili odbij / izveštaj Rust proverivača ČEKA
- 04 Referentni proverivačsertifikat vezan hashom / nezavisno prihvatanje ili odbijanje / izveštaj proverivača bez izvora ČEKA
- 05 Izveštaj o aksiomimaprovereni paket / axiom_report_hash / inventar pretpostavki ČEKA
Ishod
Objašnjavajući tok još nije pokrenut.Pokrenite objašnjenje da redom označite put provere bez izvora.
Registar tvrdnji
Odvojite dokaze, vremenski osetljive činjenice i tvrdnje o granici.
Stranica se ne oslanja na neprecizan istraživački tekst. Svaka javna tvrdnja vezana je za lokalni snimak istine, izvor i radnju objavljivanja.
| Tvrdnja | Javna formulacija | Stanje | Izvor | Radnja objavljivanja |
|---|---|---|---|---|
| CL-001 | NPA stavlja sertifikat na prvo mesto: granica koja se može revidirati jeste kanonski .npcert artefakt i put provere oko njega. | Proverena javna tvrdnja | S01 / 2026-07-02 | Pregledati kada se README promeni. |
| CL-002 | Javna ponovna provera od 2026-07-02 pronašla je najnoviju git oznaku NPA repozitorijuma na v0.2.0. README fajlovi povezanih paketa i dalje prikazuju pinove specifične za repozitorijum, pa formulacija verzije ostaje ograničena na pojedinačni repozitorijum. | Proverena javna ponovna provera | S01 / S02 / 2026-07-02 | Formulaciju oznake zadržati u okviru odgovarajućeg repozitorijuma. |
| CL-003 | Lokalni snimak istine beleži pinovanje za Rust 1.95.0 alatni lanac; to se ne koristi kao marketinška tvrdnja. | Provereno, vremenski osetljivo | S01 / 2026-07-02 | Ponovo proveriti ako se prikazuje verzija alatnog lanca. |
| CL-004 | NPA nije praktična zamena za Lean ili Rocq. Ta granica mora ostati vidljiva uz svako poređenje. | Proverena tvrdnja o granici | S01 / S03 / S05 / 2026-07-02 | Zadržati napomenu o ograničenju. |
| CL-005 | npa-std i npa-mathlib su odvojeni javni repozitorijumi paketa teorema u organizaciji finitefield-org. | Proverena javna tvrdnja | S01 / S02 / 2026-07-02 | Ponovo proveriti vidljivost repozitorijuma ako se objava odloži ili se repozitorijumi promene. |
| CL-006 | Repozitorijumi npa, npa-std i npa-mathlib javno izlažu Apache-2.0 licencu kroz svoje LICENSE metapodatke. | Proverena javna tvrdnja | S01 / S02 / 2026-07-02 | Ponovo proveriti LICENSE pri većem izdanju. |
Repozitorijumi i licence
Kod, repozitorijumi paketa i vidljivost organizacije moraju ostati izričiti.
Linkovi ka repozitorijumima su pokazivači na javne izvore, a ne garancija da je trenutna stranica usklađena sa najnovijim stanjem na GitHubu.
4 repozitorijuma prikazano
finitefield-org
npa
Alatni lanac za pomoć pri dokazima i verifikaciju sa sertifikatom na prvom mestu.
- Licenca
- Apache-2.0, proverena iz LICENSE fajla 2026-07-02.
- Provera
- Najnovija git oznaka: v0.2.0. Najnovije GitHub izdanje nije objavljeno. Trenutna README referenca alatnog lanca: NPA_GIT_TAG=v0.2.0.
eksperimentalnoRust / OCamlsertifikat na prvom mestu
Otvori repozitorijum
finitefield-org
npa-std
Repozitorijum standardnog paketa teorema za NPA izvore dokaza.
- Licenca
- Apache-2.0, proverena iz LICENSE fajla 2026-07-02.
- Provera
- Najnovija git oznaka i GitHub izdanje: v0.1.0. Verzija README metapodataka paketa: 0.1.0; pin alatnog lanca paketa: NPA_GIT_TAG=v0.1.1.
eksperimentalnopaket teoremaizvor dokaza
Otvori repozitorijum
finitefield-org
npa-mathlib
Istraživački repozitorijum biblioteke formalne matematike.
- Licenca
- Apache-2.0, proverena iz LICENSE fajla 2026-07-02.
- Provera
- Najnovija git oznaka: v0.1.30. Najnovije GitHub izdanje: v0.1.9. Verzija README metapodataka paketa: 0.2.1; pin alatnog lanca paketa: NPA_GIT_TAG=v0.1.1.
istraživanjeformalna matematikabiblioteka
Otvori repozitorijum
finitefield-org
Finite Field GitHub organizacija
Javni snimak organizacije za porodicu Lab repozitorijuma.
- Licenca
- Primenjuju se licence pojedinačnih repozitorijuma
- Provera
- npa, npa-std i npa-mathlib javni su prema GitHub API očitavanju od 2026-07-02.
javni indekssnimak vidljivostiizvor
Otvori organizaciju
Nijedan repozitorijum ne odgovara trenutnoj pretrazi.
GitHub repozitorijumi su izvor za javni status koda. Licenca, trenutne oznake, javna vidljivost i formulacije o izdanjima provereni su 2026-07-02 kao završno očitavanje za M10-T14.
Kontrola ekosistema dokaza
Razjasnite uloge pre poređenja dokaznih alata.
Ovo je tabela uloga, a ne rang-lista. Lean i Rocq ostaju referentni ekosistemi asistenata za dokazivanje; NPA je prikazan kao istraživački i implementacioni rad usmeren na sertifikate.
| Stavka | Lean | Rocq | NPA |
|---|---|---|---|
| Položaj | Programski jezik otvorenog koda i asistent za dokazivanje. | Interaktivni dokazivač teorema s dugom istraživačkom istorijom. | Repozitorijum za istraživanje i implementaciju provere u kojoj je sertifikat na prvom mestu. |
| Tipična upotreba | Matematika, verifikacija softvera i programiranje. | Matematika, specifikacije, verifikacija programa i ekstrakcija. | Istraživanje dokaznih sertifikata, nezavisne provere i male pouzdane osnove. |
| Granica dokaza | Njegov sopstveni pouzdani kernel i ekosistem definišu granicu provere. | Njegov sopstveni kernel i provereni razvojni rad definišu granicu provere. | Kanonski .npcert artefakt prelazi iz generisanja u proveru. |
| Kako ova stranica to prikazuje | Referenca za učenje, poređenje i interoperabilnost. | Referenca za učenje, poređenje i metode formalizacije. | Istraživački projekat Finite Fielda, ne obećanje proizvoda. |
| Granica | I dalje je potrebno stručno znanje. | I dalje je potrebno stručno znanje. | NPA trenutno nije praktična zamena za Lean ili Rocq. |
Izvori
Objavite mapu izvora uz tumačenje.
Izvori su prikazani da čitalac može videti koje tvrdnje dolaze iz javnih repozitorijuma, zvaničnih stranica dokaznih alata i konteksta kompanije.
S01
finitefield-org/npa
Primarni izvor za svrhu NPA-a, model poverenja, formulaciju trenutne oznake repozitorijuma v0.2.0, komande, strukturu repozitorijuma i licencu.
Otvori izvor S02Finite Field GitHub organizacija
Primarni izvor za javnu vidljivost repozitorijuma, najnovije git oznake, stranice izdanja i snimak porodice Lab repozitorijuma proveren 2026-07-02.
Otvori izvor S03Zvanična stranica Leana
Primarni izvor za javno pozicioniranje Leana, proveren 2026-07-02.
Otvori izvor S04Referenca jezika Lean
Primarni izvor za teoriju zavisnih tipova i referentni kontekst kernela, proveren 2026-07-02.
Otvori izvor S05Zvanična stranica Rocq Provera
Primarni izvor za javno pozicioniranje Rocqa, proveren 2026-07-02.
Otvori izvor S06FINITE FIELD stranica kompanije
Izvor kompanije za brend Finite Field i poslovni kontekst.
Otvori izvorPitanja i odgovori
Status NPA-a i granice verifikacije.
Odgovori naglašavaju granicu poverenja pre nego što čitaoci istraživačku stranicu pomešaju sa uvedenom uslugom asistenta za dokazivanje.
Pročitajte o kompaniji01 Da li je ova stranica garancija proizvoda?
Ne. NPA je ovde prikazan kao istraživački i implementacioni repozitorijum.
02 Može li NPA zameniti Lean ili Rocq?
Ne. NPA nije praktična zamena za Lean ili Rocq.
03 Da li stranica pokreće stvarnu NPA verifikaciju?
Ne. Simulacija u pregledaču ne pokreće sam NPA, Rust, WASM niti stvarne dokazne sertifikate.
04 Šta se ovde računa kao dokaz?
Sertifikacioni artefakt, deterministički hashovi, rezultat Rust kernela/proverivača, rezultat referentnog proverivača bez izvora i izveštaj o aksiomima čine dokaze na strani provere.
05 Koje činjenice treba ponovo proveravati?
Trenutna javna verzija, vidljivost repozitorijuma, pinovi alatnog lanca, tekst licence i formulacije iz izvora ponovo su provereni 2026-07-02.
Od dokazne discipline do operacija
Koristite istu disciplinu dokaza kada poslovnoj odluci treba verovati.
Za poslovne sisteme korisna lekcija nije da se dokazivanje teorema doda svuda. Korisno je odlučiti šta se mora generisati, proveriti, zabeležiti, ispraviti i odobriti uz ljudsku odgovornost.