NPA / sertifikatførst beviskontroll

NPA: vis grensen for bevisevidens før et resultat stoles på.

Denne siden gjenoppbygger NPA-delen fra Math Lab som en selvstendig evidensside: offentlig status, tillitsmodell, beviskontrollflyt, påstandsregister, kodearkiver, kilder og eksplisitt språk om at NPA ikke er en erstatning.

Inspiser tillitsgrensen Åpne GitHub-kodearkiv

Offentlig status: Forskningskodearkiv; Vist som forskning og implementering, ikke som en produksjonsgarantitjeneste.
Offentlig nykontroll: 2026-07-02 / NPA v0.2.0; Nyeste git-tagger kontrollert: npa v0.2.0, npa-std v0.1.0, npa-mathlib v0.1.30.
Lisens: Apache-2.0; Apache-2.0 ble bekreftet for npa, npa-std og npa-mathlib 2026-07-02.

Offentlig nykontroll: 2026-07-02. Nyeste git-tag for NPA-kodearkivet er v0.2.0; npa-std er v0.1.0; npa-mathlib er v0.1.30. README-låsing for pakker vises som kodearkivspesifikk kontekst og slås ikke sammen til én NPA-versjonspåstand.

Forhåndsvisning av NPA-evidensside med sertifikatkontroll og inspeksjon av tillitsgrense — Visualiseringen er en statisk forhåndsvisning av sertifikatkontrollresultatet og forklaringen av tillitsgrensen. Den er ikke et levende NPA-spor.

Offentlig status

Oppgi hva som er offentlig, hva som er evidens, og når det ble kontrollert på nytt.

Denne siden gjør grunnlaget synlig: et lokalt sannhetsøyeblikksbilde, en offentlig kodearkivkilde og datoen for endelig førlanserings-tilbakelesing.

Offentlig status

Forsknings- og implementeringskodearkiv

GitHub-kodearkivet er offentlig, men denne siden beskriver et forsknings- og implementeringskodearkiv, ikke en driftssatt tjeneste.

Offentlig nykontroll

2026-07-02

Den offentlige kildetilbakelesingen ble fullført 2026-07-02. Den opprinnelige kilderekonstruksjonen bruker fortsatt det lokale sannhetsøyeblikksbildet fra 2026-06-21.

Evidens

Sertifikater og hasher

Kildeøyeblikksbildet registrerer kanonisk .npcert, certificate_hash, export_hash, axiom_report_hash og kontrollørvurderinger.

Lisens

Apache-2.0 bekreftet

Apache-2.0 ble bekreftet for npa, npa-std og npa-mathlib gjennom offentlig LICENSE-metadata 2026-07-02.

Grense

NPA er ikke en praktisk erstatning for Lean eller Rocq. Den distribuerte inspeksjonssimuleringen i nettleseren kjører ikke NPA selv. Offentlige tagger, lisens og kodearkivsynlighet ble kontrollert 2026-07-02 for endelig publiseringstilbakelesing.

Tillitsgrense

Flytt bare et kanonisk sertifikat over evidensgrensen.

Grensen handler ikke om hvilket verktøy som virker avansert. Den handler om hvilket artefakt som får bli evidens etter uavhengig kontroll.

Parser, elaborator, taktikker, automatisering, teoremsøk, plugins, AI-systemer, kildefiler, replay-filer, teoremindekser, publiseringsplaner, CI-status, utgivelsessider og registry-metadata blir på den ikke-betrodde kandidatsiden.

Beviskontrollflyt / forklarende simulering

Vis den nøyaktige kontrollflyten fra sertifikatbyte til kontrollevidens.

Nettlesersimuleringen kjører ikke NPA selv, Rust, WASM eller ekte bevissertifikater. Den visualiserer den kildefrie kontrollrekkefølgen som ekte artefakter må oppfylle.

CLI-evidensvei

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

NPA / audit trace KLAR

01 Sertifikatformatkanoniske .npcert-byte / parsbar sertifikatfil / formatkontroll VENTER
02 Sertifikat-hashsertifikatbyte / certificate_hash / deterministisk digest VENTER
03 Kjernevurderingsertifikat / godta eller avvis / Rust-verifikatorrapport VENTER
04 Referansekontrollørhash-låst sertifikat / uavhengig godta eller avvis / kildefri kontrollørrapport VENTER
05 Aksiomrapportkontrollert pakke / axiom_report_hash / antakelsesoversikt VENTER

Vurdering

Den forklarende kontrollflyten er ikke kjørt ennå.

Kjør forklaringen for å markere den kildefrie kontrollveien i rekkefølge.

Påstandsregister

Skill mellom evidens, tidsfølsomme fakta og grensepåstander.

Siden bygger ikke på løs forskningsprosa. Hver offentlig uttalelse er knyttet til et lokalt sannhetsøyeblikksbilde, en kilde og et publiseringstiltak.

Påstand	Offentlig formulering	Status	Kilde	Publiseringstiltak
CL-001	NPA er sertifikatførst: den reviderbare grensen er det kanoniske .npcert-artefaktet og kontrollveien rundt det.	Bekreftet offentlig påstand	S01 / 2026-07-02	Gå gjennom på nytt når README endres.
CL-002	Den offentlige nykontrollen 2026-07-02 fant at nyeste git-tag for NPA-kodearkivet var v0.2.0. README-ene for relaterte pakker viser fortsatt kodearkivspesifikke låsinger, så versjonsformuleringen holdes avgrenset per kodearkiv.	Bekreftet offentlig nykontroll	S01 / S02 / 2026-07-02	Hold taggformuleringen avgrenset per kodearkiv.
CL-003	Det lokale sannhetsøyeblikksbildet registrerer en Rust 1.95.0-verktøykjedelås; den brukes ikke som markedsføringspåstand.	Bekreftet, tidsfølsom	S01 / 2026-07-02	Kontroller på nytt hvis verktøykjedeversjonen vises.
CL-004	NPA er ikke en praktisk erstatning for Lean eller Rocq. Denne grensen må være synlig ved siden av enhver sammenligning.	Bekreftet grensepåstand	S01 / S03 / S05 / 2026-07-02	Behold forbeholdet.
CL-005	npa-std og npa-mathlib er separate offentlige kodearkiver for teorempakker i finitefield-org-organisasjonen.	Bekreftet offentlig påstand	S01 / S02 / 2026-07-02	Kontroller kodearkivsynligheten på nytt hvis publisering utsettes eller kodearkivene endres.
CL-006	Kodearkivene npa, npa-std og npa-mathlib viser alle Apache-2.0-lisens gjennom offentlig LICENSE-metadata.	Bekreftet offentlig påstand	S01 / S02 / 2026-07-02	Kontroller LICENSE på nytt ved større utgivelser.

Kodearkiver og lisens

Gjør kode, pakkekodearkiver og organisasjonssynlighet eksplisitt.

Kodearkivlenker er offentlige kildepekere, ikke garantier for at gjeldende side er synkronisert med nyeste GitHub-status.

4 kodearkiver vist

finitefield-org

npa

Sertifikatførst bevisassistanse og verifikasjonsverktøykjede.

Lisens: Apache-2.0 bekreftet fra LICENSE 2026-07-02.
Verifikasjon: Nyeste git-tag: v0.2.0. Ingen nyeste GitHub-utgivelse er publisert. Gjeldende verktøykjedereferanse i README: NPA_GIT_TAG=v0.2.0.

eksperimentellRust / OCamlsertifikatførst

Åpne kodearkiv

finitefield-org

npa-std

Standard teorempakke-kodearkiv for NPA-beviskilder.

Lisens: Apache-2.0 bekreftet fra LICENSE 2026-07-02.
Verifikasjon: Nyeste git-tag og GitHub-utgivelse: v0.1.0. README-pakkemetadata versjon: 0.1.0; pakkeverktøykjedelås: NPA_GIT_TAG=v0.1.1.

eksperimentellteorempakkebeviskilde

Åpne kodearkiv

finitefield-org

npa-mathlib

Forskningskodearkiv for formelt matematikkbibliotek.

Lisens: Apache-2.0 bekreftet fra LICENSE 2026-07-02.
Verifikasjon: Nyeste git-tag: v0.1.30. Nyeste GitHub-utgivelse: v0.1.9. README-pakkemetadata versjon: 0.2.1; pakkeverktøykjedelås: NPA_GIT_TAG=v0.1.1.

forskningformell matematikkbibliotek

Åpne kodearkiv

finitefield-org

Finite Field GitHub-organisasjon

Offentlig organisasjonsøyeblikksbilde for Lab-kodearkivfamilien.

Lisens: Kodearkivspesifikke lisenser gjelder
Verifikasjon: npa, npa-std og npa-mathlib er offentlige fra GitHub API-tilbakelesingen 2026-07-02.

offentlig indekssynlighetsøyeblikksbildekilde

Åpne organisasjon

GitHub-kodearkivene er kilden for offentlig kodestatus. Lisens, gjeldende tagger, offentlig synlighet og utgivelsesformuleringer ble kontrollert 2026-07-02 som endelig M10-T14-tilbakelesing.

Sikring av bevisøkosystem

Avklar roller før bevisverktøy sammenlignes.

Dette er en rolletabell, ikke en rangering. Lean og Rocq er fortsatt referanseøkosystemer for bevisassistenter; NPA presenteres som sertifikatsentrert forsknings- og implementeringsarbeid.

Punkt	Lean	Rocq	NPA
Posisjon	Programmeringsspråk med åpen kildekode og bevisassistent.	Interaktiv teorembeviser med lang forskningshistorie.	Forsknings- og implementeringskodearkiv for sertifikatførst-kontroll.
Typisk bruk	Matematikk, programvareverifisering og programmering.	Matematikk, spesifikasjoner, programverifisering og ekstraksjon.	Forskning på bevissertifikater, uavhengig kontroll og en liten betrodd base.
Evidensgrense	Dens egen betrodde kjerne og økosystem definerer kontrollgrensen.	Dens egen kjerne og kontrollerte utviklinger definerer kontrollgrensen.	Det kanoniske .npcert-artefaktet går fra generering inn i kontroll.
Hvordan denne siden behandler det	Referanse for læring, sammenligning og interoperabilitet.	Referanse for læring, sammenligning og formaliseringsmetoder.	Finite Field-forskningsprosjekt, ikke et produktløfte.
Grense	Spesialistkunnskap er fortsatt nødvendig.	Spesialistkunnskap er fortsatt nødvendig.	NPA er ikke en praktisk erstatning for Lean eller Rocq nå.

Lean offisielt nettsted Rocq Prover offisielt nettsted NPA GitHub

Kilder

Publiser kildekartet ved siden av tolkningen.

Kilder vises slik at leseren kan se hvilke påstander som kommer fra offentlige kodearkiver, offisielle nettsteder for bevisverktøy og selskapskontekst.

S01

finitefield-org/npa

Primærkilde for NPAs formål, tillitsmodell, gjeldende v0.2.0-kodearkivtagg, kommandoer, kodearkivoppsett og lisens.

Åpne kilde S02

Finite Field GitHub-organisasjon

Primærkilde for offentlig kodearkivsynlighet, nyeste git-tagger, utgivelsessider og øyeblikksbildet av Lab-kodearkivfamilien kontrollert 2026-07-02.

Åpne kilde S03

Lean offisielt nettsted

Primærkilde for Leans offentlige posisjonering, kontrollert 2026-07-02.

Åpne kilde S04

Lean språkreferanse

Primærkilde for kontekst om avhengig typeteori og kjernereferanse, kontrollert 2026-07-02.

Åpne kilde S05

Rocq Prover offisielt nettsted

Primærkilde for Rocqs offentlige posisjonering, kontrollert 2026-07-02.

Åpne kilde S06

FINITE FIELD selskapsnettsted

Selskapskilde for Finite Field-merkevaren og forretningskontekst.

Åpne kilde

Vanlige spørsmål

NPA-status og verifikasjonsgrenser.

Svarene fremhever tillitsgrensen før lesere forveksler en forskningsside med en driftssatt bevisassistenttjeneste.

Les om selskapet

01 Er denne siden en produktgaranti?

Nei. NPA vises her som et forsknings- og implementeringskodearkiv.

02 Kan NPA erstatte Lean eller Rocq?

Nei. NPA er ikke en praktisk erstatning for Lean eller Rocq.

03 Kjører siden ekte NPA-verifikasjon?

Nei. Nettlesersimuleringen kjører ikke NPA selv, Rust, WASM eller ekte bevissertifikater.

04 Hva regnes som evidens her?

Sertifikatartefaktet, deterministiske hasher, resultatet fra Rust-kjernen/verifikatoren, resultatet fra den kildefrie referansekontrolløren og aksiomrapporten utgjør evidensen på kontrollsiden.

05 Hvilke fakta må kontrolleres på nytt?

Gjeldende offentlig versjon, kodearkivsynlighet, verktøykjedelåser, lisenstekst og kildeformuleringer ble kontrollert på nytt 2026-07-02.

Fra bevisdisiplin til drift

Bruk samme evidensdisiplin når en forretningsbeslutning må kunne stoles på.

For forretningssystemer er den nyttige lærdommen ikke å legge teorembevis inn overalt. Den er å avgjøre hva som må genereres, kontrolleres, loggføres, korrigeres og godkjennes av mennesker.

Sjekk forretningsproblemet Se prototype