NPA / Vottorðsmiðuð sönnunarathugun

NPA: sýndu mörk sönnunargagna áður en niðurstöðu er treyst.

Þessi síða endurbyggir NPA-hlutann úr Stærðfræðistofunni sem sjálfstæða sönnunargagnasíðu: opinbera stöðu, traustlíkan, sönnunarferli, fullyrðingaskrá, gagnasöfn, heimildir og skýr mörk gagnvart Lean og Rocq.

Skoða traustmörkin Opna GitHub-gagnasafn

Opinber staða: Rannsóknargagnasafn; Sýnt sem rannsókn og útfærsla, ekki sem framleiðslutryggingarþjónusta.
Opinber endurathugun: 2026-07-02 / NPA v0.2.0; Nýjustu git-merki athuguð: npa v0.2.0, npa-std v0.1.0, npa-mathlib v0.1.30.
Leyfi: Apache-2.0; Apache-2.0 var staðfest fyrir npa, npa-std og npa-mathlib 2026-07-02.

Opinber endurathugun: 2026-07-02. Nýjasta git-merki NPA-gagnasafnsins er v0.2.0; npa-std er v0.1.0; npa-mathlib er v0.1.30. README-festingar pakka eru sýndar sem samhengi hvers gagnasafns og eru ekki sameinaðar í eina útgáfufullyrðingu um NPA.

Forskoðun NPA-sönnunargagnasíðu sem sýnir vottorðsathugun og skoðun traustmarka — Myndin er föst forskoðun á niðurstöðu vottorðsathugunar og skýringu traustmarka. Hún er ekki lifandi keyrsluspor úr NPA.

Opinber staða

Segðu skýrt hvað er opinbert, hvað er sönnunargagn og hvenær það var endurathugað.

Síðan gerir grunn sinn sýnilegan: staðbundna staðreyndaskrá, opinbera heimild í gagnasafni og lokadagsetningu endurlestrar fyrir birtingu.

Opinber staða

Rannsóknar- og útfærslugagnasafn

GitHub-gagnasafnið er opinbert, en þessi síða lýsir rannsóknar- og útfærslugagnasafni, ekki keyrðri þjónustu.

Opinber endurathugun

2026-07-02

Endurlestur opinberra heimilda lauk 2026-07-02. Upprunaleg endurgerð heimilda notar enn staðbundna staðreyndaskrá frá 2026-06-21.

Sönnunargögn

Vottorð og tætigildi

Heimildastöðumyndin skráir staðlað .npcert, certificate_hash, export_hash, axiom_report_hash og úrskurði athugara.

Leyfi

Apache-2.0 staðfest

Apache-2.0 var staðfest fyrir npa, npa-std og npa-mathlib með opinberum LICENSE-lýsigögnum 2026-07-02.

Mörk

NPA er ekki hagnýtur staðgengill Lean eða Rocq. Vafrahermunin sem fylgir síðunni keyrir ekki NPA sjálft. Opinber merki, leyfi og sýnileiki gagnasafna voru athuguð 2026-07-02 fyrir lokaendurlestur fyrir birtingu.

Traustmörk

Flyttu aðeins staðlað vottorð yfir sönnunargagnamörkin.

Mörkin snúast ekki um hvaða verkfæri virðist fullkomnast. Þau snúast um hvaða gripur má verða sönnunargagn eftir óháða athugun.

Þáttari, útfærari, taktík, sjálfvirkni, setningaleit, viðbætur, gervigreindarkerfi, frumskrár, endurspilunarskrár, setningavísar, birtingaráætlanir, CI-staða, útgáfusíður og skráningarlýsigögn eru áfram á ótraustu frambjóðendahliðinni.

Sönnunarferli / skýringarhermun

Sýndu nákvæma leið frá vottorðsbætum til athuganlegra sönnunargagna.

Vafrahermunin keyrir ekki NPA sjálft, Rust, WASM eða raunveruleg sönnunarvottorð. Hún sýnir frumkóðalausa athugunarröð sem raunverulegir gripir þurfa að standast.

CLI-leið sönnunargagna

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

NPA / úttektarslóð TILBÚIÐ

01 Snið vottorðsstaðlaðir .npcert-bætar / lesanlegt vottorð / sniðathugun BÍÐ
02 Tætigildi vottorðsvottorðsbætar / certificate_hash / ákvarðanlegt tætigildi BÍÐ
03 Úrskurður kjarnavottorð / samþykkt eða höfnun / skýrsla Rust-sannreynis BÍÐ
04 Viðmiðunarathugarivottorð fest með tætigildi / óháð samþykkt eða höfnun / skýrsla frumkóðalauss athugara BÍÐ
05 Frumsetningaskýrslaathugaður pakki / axiom_report_hash / forsenduyfirlit BÍÐ

Úrskurður

Skýringarferlið hefur ekki verið keyrt enn.

Keyrðu skýringuna til að merkja frumkóðalausu athugunarleiðina í réttri röð.

Fullyrðingaskrá

Aðgreindu sönnunargögn, tímaviðkvæmar staðreyndir og afmörkunarfullyrðingar.

Síðan byggir ekki á lauslegum rannsóknartexta. Hver opinber fullyrðing er tengd staðbundinni staðreyndaskrá, heimild og birtingaraðgerð.

Fullyrðing	Opinbert orðalag	Staða	Heimild	Birtingaraðgerð
CL-001	NPA er vottorðsmiðað: úttektarmörkin eru staðlaði .npcert-gripurinn og athugunarleiðin í kringum hann.	Staðfest opinber fullyrðing	S01 / 2026-07-02	Endurskoða þegar README breytist.
CL-002	Opinber endurathugun 2026-07-02 fann nýjasta git-merki NPA-gagnasafnsins sem v0.2.0. README-skjöl tengdra pakka sýna enn festingar hvers gagnasafns, þannig að útgáfuorðalagið er afmarkað eftir gagnasafni.	Staðfest opinber endurathugun	S01 / S02 / 2026-07-02	Halda orðalagi merkja afmörkuðu eftir gagnasafni.
CL-003	Staðbundna staðreyndaskráin skráir Rust 1.95.0 verkfærakeðjufestingu; hún er ekki notuð sem markaðsfullyrðing.	Staðfest, tímaviðkvæmt	S01 / 2026-07-02	Endurathuga ef útgáfa verkfærakeðju er birt.
CL-004	NPA er ekki hagnýtur staðgengill Lean eða Rocq. Þessi mörk þurfa að sjást við hlið hvers samanburðar.	Staðfest afmörkunarfullyrðing	S01 / S03 / S05 / 2026-07-02	Halda fyrirvaranum.
CL-005	npa-std og npa-mathlib eru aðskilin opinber setningapakkagagnasöfn í finitefield-org stofnuninni.	Staðfest opinber fullyrðing	S01 / S02 / 2026-07-02	Endurathuga sýnileika gagnasafna ef birting tefst eða gagnasöfn breytast.
CL-006	Gagnasöfnin npa, npa-std og npa-mathlib birta hvert um sig Apache-2.0 leyfi í opinberum LICENSE-lýsigögnum.	Staðfest opinber fullyrðing	S01 / S02 / 2026-07-02	Endurathuga LICENSE við stóra útgáfu.

Gagnasöfn og leyfi

Haltu kóða, pakkagagnasöfnum og sýnileika stofnunar skýrum.

Tenglar á gagnasöfn eru vísanir í opinberar heimildir, ekki trygging fyrir því að síðan sé samstillt við nýjustu stöðu GitHub.

4 gagnasöfn sýnd

finitefield-org

npa

Vottorðsmiðuð verkfærakeðja fyrir sönnunaraðstoð og sannreynslu.

Leyfi: Apache-2.0 staðfest úr LICENSE 2026-07-02.
Staðfesting: Nýjasta git-merki: v0.2.0. Engin nýjasta GitHub-útgáfa er birt. README vísar nú í verkfærakeðju: NPA_GIT_TAG=v0.2.0.

tilraunRust / OCamlvottorðsmiðað

Opna gagnasafn

finitefield-org

npa-std

Staðlað setningapakkagagnasafn fyrir NPA-sönnunarfrumskrár.

Leyfi: Apache-2.0 staðfest úr LICENSE 2026-07-02.
Staðfesting: Nýjasta git-merki og GitHub-útgáfa: v0.1.0. README-pakkalýsigögn: 0.1.0; verkfærakeðjufesting pakka: NPA_GIT_TAG=v0.1.1.

tilraunsetningapakkisönnunarfrumskrár

Opna gagnasafn

finitefield-org

npa-mathlib

Rannsóknargagnasafn fyrir formlegt stærðfræðisafn.

Leyfi: Apache-2.0 staðfest úr LICENSE 2026-07-02.
Staðfesting: Nýjasta git-merki: v0.1.30. Nýjasta GitHub-útgáfa: v0.1.9. README-pakkalýsigögn: 0.2.1; verkfærakeðjufesting pakka: NPA_GIT_TAG=v0.1.1.

rannsóknformleg stærðfræðisafn

Opna gagnasafn

finitefield-org

Finite Field GitHub-stofnun

Opinber stöðumynd stofnunar fyrir gagnasafnafjölskyldu Stærðfræðistofunnar.

Leyfi: Leyfi fara eftir hverju gagnasafni.
Staðfesting: npa, npa-std og npa-mathlib eru opinber samkvæmt GitHub API-endurlestri 2026-07-02.

opinbert yfirlitsýnileikastöðumyndheimild

Opna stofnun

GitHub-gagnasöfnin eru heimildin fyrir opinbera kóðastöðu. Leyfi, núverandi merki, opinber sýnileiki og útgáfuorðalag voru athuguð 2026-07-02 í lokaendurskoðun M10-T14.

Vörn fyrir sönnunarkerfi

Skýrðu hlutverk áður en sönnunarverkfæri eru borin saman.

Þetta er hlutverkattafla, ekki röðun. Lean og Rocq eru áfram viðmiðunarvistkerfi sönnunaraðstoðara; NPA er sett fram sem vottorðsmiðuð rannsóknar- og útfærsluvinna.

Atriði	Lean	Rocq	NPA
Staða	Opið forritunarmál og sönnunaraðstoðari.	Gagnvirkur setningasannari með langa rannsóknarsögu.	Rannsóknar- og útfærslugagnasafn fyrir vottorðsmiðaða athugun.
Dæmigerð notkun	Stærðfræði, hugbúnaðarsannprófun og forritun.	Stærðfræði, forskriftir, forritasannprófun og útdráttur.	Rannsóknir á sönnunarvottorðum, óháðri athugun og litlum traustum grunni.
Mörk sönnunargagna	Eigin traustur kjarni og vistkerfi skilgreina athugunarmörkin.	Eigin kjarni og athuguð þróun skilgreina athugunarmörkin.	Staðlaði .npcert-gripurinn fer frá gerð yfir í athugun.
Hvernig þessi síða notar það	Viðmið fyrir nám, samanburð og samvirkni.	Viðmið fyrir nám, samanburð og formfestingaraðferðir.	Rannsóknarverkefni Finite Field, ekki vöruloforð.
Mörk	Sérfræðiþekking er enn nauðsynleg.	Sérfræðiþekking er enn nauðsynleg.	NPA er ekki hagnýtur staðgengill Lean eða Rocq að svo stöddu.

Opinber vefsíða Lean Opinber vefsíða Rocq Prover NPA á GitHub

Heimildir

Birtu heimildakortið við hlið túlkunarinnar.

Heimildir eru sýndar svo lesandinn sjái hvaða fullyrðingar koma úr opinberum gagnasöfnum, opinberum síðum sönnunarverkfæra og fyrirtækjasamhengi.

S01

finitefield-org/npa

Aðalheimild fyrir tilgang NPA, traustlíkan, orðalag núverandi gagnasafnsmerkis v0.2.0, skipanir, uppbyggingu gagnasafns og leyfi.

Opna heimild S02

Finite Field GitHub-stofnun

Aðalheimild fyrir opinberum sýnileika gagnasafna, nýjustu git-merkjum, útgáfusíðum og stöðumynd gagnasafnafjölskyldu Stærðfræðistofunnar sem var athuguð 2026-07-02.

Opna heimild S03

Opinber vefsíða Lean

Aðalheimild fyrir opinberri staðsetningu Lean, athuguð 2026-07-02.

Opna heimild S04

Lean-máltilvísun

Aðalheimild fyrir samhengi háðrar gerðafræði og kjarna, athuguð 2026-07-02.

Opna heimild S05

Opinber vefsíða Rocq Prover

Aðalheimild fyrir opinberri staðsetningu Rocq, athuguð 2026-07-02.

Opna heimild S06

FINITE FIELD fyrirtækjasíða

Fyrirtækjaheimild fyrir vörumerki Finite Field og viðskiptasamhengi.

Opna heimild

Algengar spurningar

Staða NPA og mörk sannprófunar.

Svörin leggja áherslu á traustmörkin áður en lesendur rugla rannsóknarsíðu saman við keyrða þjónustu fyrir sönnunaraðstoð.

Lesa um fyrirtækið

01 Er þessi síða vörutrygging?

Nei. NPA er hér sýnt sem rannsóknar- og útfærslugagnasafn. Verkefni viðskiptavina þurfa áfram sérstakar kröfur, áhættu, ábyrgð og samþykkisviðmið.

02 Getur NPA komið í stað Lean eða Rocq?

Nei. NPA er ekki hagnýtur staðgengill Lean eða Rocq. Síðan heldur þessum mörkum sýnilegum vegna þess að þau skipta máli fyrir væntingar.

03 Keyrir síðan raunverulega NPA-sannreynslu?

Nei. Vafrahermunin keyrir ekki NPA sjálft, Rust, WASM eða raunveruleg sönnunarvottorð. Hún útskýrir skoðunarröðina.

04 Hvað telst sönnunargagn hér?

Vottorðsgripurinn, ákvarðanleg tætigildi, niðurstaða Rust-kjarna/sannreynis, niðurstaða frumkóðalauss viðmiðunarathugara og frumsetningaskýrsla mynda sönnunargögn athugunarhliðinnar.

05 Hvaða staðreyndir þarf að endurathuga?

Núverandi opinbera útgáfu, sýnileika gagnasafna, verkfærakeðjufestingar, leyfistexta og heimildaorðalag var endurathugað 2026-07-02 og ætti að athuga aftur ef birting tefst eða gagnasöfn breytast.

Frá sönnunaraga til rekstrar

Notaðu sama aga sönnunargagna þegar viðskiptaákvörðun þarf að vera traust.

Í viðskiptakerfum er lærdómurinn ekki að bæta setningasönnun við allt. Hann er að ákveða hvað þarf að búa til, athuga, skrá, leiðrétta og samþykkja af fólki.

Athuga rekstrarvandann Skoða frumgerð