NPA / certifikatförst-beviskontroll

NPA: visa bevisgränsen innan ett resultat betros.

Denna sida återskapar NPA-avsnittet från Matematiklabbet som en fristående evidenssida: offentlig status, förtroendemodell, bevispipeline, påståenderegister, repon, källor och tydlig text om att NPA inte är en ersättning.

Granska förtroendegränsen Öppna GitHub-repot

Offentlig status: Forskningsrepo; Visas som forskning och implementering, inte som en produktionssäkringstjänst.
Offentlig omkontroll: 2026-07-02 / NPA v0.2.0; Senaste kontrollerade git-taggar: npa v0.2.0, npa-std v0.1.0, npa-mathlib v0.1.30.
Licens: Apache-2.0; Apache-2.0 verifierades för npa, npa-std och npa-mathlib 2026-07-02.

Offentlig omkontroll: 2026-07-02. Senaste git-taggen i NPA-repot är v0.2.0; npa-std är v0.1.0; npa-mathlib är v0.1.30. README-låsningar visas som repospecifik kontext och slås inte samman till ett enda påstående om NPA-versionen.

Förhandsvisning av NPA-evidenssidan med certifikatkontroll och granskning av förtroendegränsen — Bilden är en statisk förhandsvisning av certifikatkontrollens resultat och förklaringen av förtroendegränsen. Den är inte en NPA-spårning i realtid.

Offentlig status

Ange vad som är offentligt, vad som är evidens och när det kontrollerades igen.

Sidan synliggör sin grund: en lokal referensbild, en offentlig repokälla och datumet för den slutliga kontrollen före lansering.

Offentlig status

Forsknings- och implementeringsrepo

GitHub-repot är offentligt, men sidan beskriver ett forsknings- och implementeringsrepo, inte en driftsatt tjänst.

Offentlig omkontroll

2026-07-02

Kontrollen av offentliga källor slutfördes 2026-07-02. Den ursprungliga källrekonstruktionen använder fortfarande den lokala referensbilden från 2026-06-21.

Evidens

Certifikat och hashvärden

Källbilden registrerar kanonisk .npcert, certificate_hash, export_hash, axiom_report_hash och kontrollutslag.

Licens

Apache-2.0 verifierad

Apache-2.0 verifierades för npa, npa-std och npa-mathlib genom offentliga LICENSE-metadata 2026-07-02.

Gräns

NPA är inte en praktisk ersättning för Lean eller Rocq. Den distribuerade inspektionssimuleringen i webbläsaren kör inte NPA självt. Offentliga taggar, licens och reposynlighet kontrollerades 2026-07-02 för den slutliga omkontrollen före publicering.

Förtroendegräns

Flytta endast ett kanoniskt certifikat över evidensgränsen.

Gränsen handlar inte om vilket verktyg som ser sofistikerat ut, utan om vilken artefakt som får bli evidens efter oberoende kontroll.

Parser, elaborator, taktiker, automatisering, teoremsökning, insticksprogram, AI-system, källfiler, replayfiler, teoremindex, publiceringsplaner, CI-status, releasesidor och registermetadata stannar på den opålitliga kandidatsidan.

Bevispipeline / förklarande simulering

Visa den exakta pipelinen från certifikatbyte till kontrollevidens.

Webbläsarsimuleringen kör varken NPA självt, Rust, WASM eller verkliga beviscertifikat. Den visar den källfria kontrollordning som verkliga artefakter måste uppfylla.

Evidensväg i CLI

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

NPA / granskningsspår REDO

01 Certifikatformatkanoniska .npcert-byte / parsbart certifikat / formatkontroll VÄNTA
02 Certifikatets hashcertifikatbyte / certifikat_hash / deterministiskt digest VÄNTA
03 Kärnans utlåtandecertifikat / godkännande eller avvisning / rapport från Rust-verifieraren VÄNTA
04 Referenskontrollhashlåst certifikat / oberoende godkännande eller avvisning / rapport från källfri kontroll VÄNTA
05 Axiomrapportkontrollerat paket / axiomrapport_hash / inventering av antaganden VÄNTA

Utlåtande

Den förklarande pipelinen har ännu inte körts.

Kör förklaringen för att markera den källfria kontrollvägen i ordning.

Påståenderegister

Håll isär evidens, tidskänsliga fakta och gränspåståenden.

Sidan förlitar sig inte på löst formulerad forskningstext. Varje offentligt uttalande är kopplat till en lokal referensbild, en källa och en åtgärd inför publicering.

Påstående	Offentlig formulering	Läge	Källa	Åtgärd inför publicering
CL-001	NPA sätter certifikatet främst: den granskningsbara gränsen utgörs av den kanoniska .npcert-artefakten och kontrollvägen runt den.	Verifierat offentligt påstående	S01 / 2026-07-02	Granska igen när README ändras.
CL-002	Den offentliga omkontrollen den 2026-07-02 visade att den senaste Git-taggen i NPA-repot var v0.2.0. README-filerna för relaterade paket visar fortfarande repospecifika bindningar, så versionsformuleringen förblir avgränsad till respektive repo.	Verifierad offentlig omkontroll	S01 / S02 / 2026-07-02	Håll taggformuleringen avgränsad till respektive repo.
CL-003	Den lokala referensbilden registrerar en bindning till verktygskedjan Rust 1.95.0; den används inte som ett marknadsföringspåstående.	Verifierat, tidskänsligt	S01 / 2026-07-02	Kontrollera igen om verktygskedjans version visas.
CL-004	NPA är inte en praktisk ersättning för Lean eller Rocq. Denna gräns måste förbli synlig vid varje jämförelse.	Verifierat gränspåstående	S01 / S03 / S05 / 2026-07-02	Behåll ansvarsfriskrivningen.
CL-005	npa-std och npa-mathlib är separata offentliga repositorier för teorempaket i organisationen finitefield-org.	Verifierat offentligt påstående	S01 / S02 / 2026-07-02	Kontrollera repositoriernas synlighet igen om publiceringen fördröjs eller om repositorierna ändras.
CL-006	Repositorierna npa, npa-std och npa-mathlib visar var och en licensen Apache-2.0 genom sina offentliga LICENSE-metadata.	Verifierat offentligt påstående	S01 / S02 / 2026-07-02	Kontrollera LICENSE igen vid en större utgåva.

Repon och licens

Gör kod, paketrepon och organisationens synlighet tydliga.

Repolänkarna pekar på offentliga källor men garanterar inte att sidan är synkroniserad med den senaste GitHub-statusen.

4 visade repon

finitefield-org

npa

Verktygskedja för certifikatcentrerad bevisassistans och verifiering.

Licens: Apache-2.0 verifierad från LICENSE 2026-07-02.
Verifiering: Senaste git-taggen: v0.2.0. Ingen senaste GitHub-release är publicerad. Aktuell referens för verktygskedjan i README: NPA_GIT_TAG=v0.2.0.

experimentellRust / OCamlcertifikat först

Öppna repo

finitefield-org

npa-std

Repo för standardpaketet med teorem för NPA-beviskällor.

Licens: Apache-2.0 verifierad från LICENSE 2026-07-02.
Verifiering: Senaste git-tagg och GitHub-release: v0.1.0. Paketmetadata-version i README: 0.1.0; paketets låsning av verktygskedjan: NPA_GIT_TAG=v0.1.1.

experimentellteorempaketbeviskälla

Öppna repo

finitefield-org

npa-mathlib

Forskningsrepo för ett bibliotek med formell matematik.

Licens: Apache-2.0 verifierad från LICENSE 2026-07-02.
Verifiering: Senaste git-taggen: v0.1.30. Senaste GitHub-release: v0.1.9. Paketmetadata-version i README: 0.2.1; paketets låsning av verktygskedjan: NPA_GIT_TAG=v0.1.1.

forskningformell matematikbibliotek

Öppna repo

finitefield-org

Finite Fields GitHub-organisation

Offentlig ögonblicksbild av organisationen för Lab-repofamiljen.

Licens: Repospecifika licenser gäller
Verifiering: npa, npa-std och npa-mathlib är offentliga enligt omkontrollen via GitHub API 2026-07-02.

offentligt indexögonblicksbild av synlighetkälla

Öppna organisationen

GitHub-repona är källan för kodens offentliga status. Licens, aktuella taggar, offentlig synlighet och releaseformulering kontrollerades 2026-07-02 i den slutliga M10-T14-omkontrollen.

Skydd för bevisekosystemet

Klargör rollerna innan bevisverktyg jämförs.

Detta är en rolltabell, inte en rangordning. Lean och Rocq förblir referensekosystem för bevisassistenter; NPA presenteras som certifikatcentrerat forsknings- och implementeringsarbete.

Objekt	Lean	Rocq	NPA
Placering	Programmeringsspråk med öppen källkod och bevisassistent.	Interaktiv teorembevisare med en lång forskningshistoria.	Forsknings- och implementeringsrepo för certifikatcentrerad kontroll.
Typisk användning	Matematik, programvaruverifiering och programmering.	Matematik, specifikationer, programverifiering och extraktion.	Forskning om beviscertifikat, oberoende kontroll och en liten betrodd bas.
Evidensgräns	Dess eget betrodda kärnsystem och ekosystem definierar kontrollgränsen.	Dess eget kärnsystem och kontrollerade utvecklingar definierar kontrollgränsen.	Den kanoniska .npcert-artefakten går från generering till kontroll.
Så behandlar sidan det	Referens för lärande, jämförelse och interoperabilitet.	Referens för lärande, jämförelse och formaliseringsmetoder.	Finite Field-forskningsprojekt, inte ett produktlöfte.
Gräns	Specialistkunskap krävs fortfarande.	Specialistkunskap krävs fortfarande.	NPA är för närvarande inte en praktisk ersättning för Lean eller Rocq.

Leans officiella webbplats Rocq Provers officiella webbplats NPA GitHub

Källor

Publicera källkartan bredvid tolkningen.

Källorna visas så att läsaren kan se vilka påståenden som kommer från offentliga repon, officiella webbplatser för bevisverktyg och företagskontext.

S01

finitefield-org/npa

Primär källa för NPA:s syfte, förtroendemodell, formulering av aktuell repotagg v0.2.0, kommandon, repostruktur och licens.

Öppna källa S02

Finite Fields GitHub-organisation

Primär källa för offentlig reposynlighet, senaste git-taggar, releasesidor och ögonblicksbilden av Lab-repofamiljen kontrollerad 2026-07-02.

Öppna källa S03

Leans officiella webbplats

Primär källa för Leans offentliga positionering, kontrollerad 2026-07-02.

Öppna källa S04

Leans språkreferens

Primär källa för kontext om beroende typteori och kärnreferens, kontrollerad 2026-07-02.

Öppna källa S05

Rocq Provers officiella webbplats

Primär källa för Rocqs offentliga positionering, kontrollerad 2026-07-02.

Öppna källa S06

FINITE FIELD företagswebbplats

Företagskälla för varumärket Finite Field och verksamhetskontexten.

Öppna källa

FAQ

NPA-status och verifieringsgränser.

Svaren betonar förtroendegränsen innan läsaren förväxlar en forskningssida med en driftsatt bevisassistenttjänst.

Läs om företaget

01 Är denna sida en produktgaranti?

Nej. NPA visas här som ett forsknings- och implementeringsrepo.

02 Kan NPA ersätta Lean eller Rocq?

Nej. NPA är inte en praktisk ersättning för Lean eller Rocq.

03 Kör sidan en verklig NPA-verifiering?

Nej. Webbläsarsimuleringen kör varken NPA självt, Rust, WASM eller verkliga beviscertifikat.

04 Vad räknas som evidens här?

Certifikatartefakten, deterministiska hashvärden, resultatet från Rust-kärnan/verifieraren, resultatet från den källfria referenskontrollen och axiomrapporten utgör evidensen på kontrollsidan.

05 Vilka fakta behöver kontrolleras igen?

Aktuell offentlig version, reposynlighet, låsningar av verktygskedjan, licenstext och källformulering kontrollerades på nytt 2026-07-02.

Från bevisdisciplin till verksamhet

Använd samma evidensdisciplin när ett verksamhetsbeslut måste vara tillförlitligt.

För verksamhetssystem är den användbara lärdomen inte att lägga till teorembevisning överallt. Det handlar om att avgöra vad människor måste generera, kontrollera, logga, korrigera och godkänna.

Kontrollera verksamhetsproblemet Visa prototyp