NPA / Sprawdzanie dowodów od certyfikatu

NPA: pokaż granicę dowodową przed zaufaniem wynikowi.

Ta strona odtwarza sekcję NPA z Laboratorium matematycznego jako niezależną stronę dowodową: stan publiczny, model zaufania, przepływ dowodowy, rejestr twierdzeń, repozytoria, źródła i wyraźne stwierdzenie, że NPA nie jest zamiennikiem.

Sprawdź granicę zaufania Otwórz repozytorium GitHub

Stan publiczny: Repozytorium badawcze; Przedstawione jako badania i implementacja, nie jako usługa zapewnienia produkcyjnego.
Publiczna ponowna kontrola: 2026-07-02 / NPA v0.2.0; Sprawdzone najnowsze tagi git: npa v0.2.0, npa-std v0.1.0, npa-mathlib v0.1.30.
Licencja: Apache-2.0; Apache-2.0 zweryfikowano dla npa, npa-std i npa-mathlib 2026-07-02.

Publiczna ponowna kontrola: 2026-07-02. Najnowszy tag git repozytorium NPA to v0.2.0; npa-std to v0.1.0; npa-mathlib to v0.1.30. Przypięcia z README pakietów są pokazane jako kontekst właściwy dla repozytorium i nie są łączone w jedno twierdzenie o wersji NPA.

Podgląd strony dowodowej NPA pokazujący sprawdzanie certyfikatu i inspekcję granicy zaufania — Grafika jest statycznym podglądem wyniku sprawdzania certyfikatu i wyjaśnienia granicy zaufania. Nie jest śladem NPA na żywo.

Stan publiczny

Wskaż, co jest publiczne, co stanowi dowód i kiedy zostało ponownie sprawdzone.

Ta strona ujawnia swoją podstawę: lokalny obraz stanu faktycznego, publiczne źródło w repozytorium i datę końcowego odczytu przed uruchomieniem.

Stan publiczny

Repozytorium badań i implementacji

Repozytorium GitHub jest publiczne, ale ta strona opisuje repozytorium badań i implementacji, nie wdrożoną usługę.

Publiczna ponowna kontrola

2026-07-02

Ponowny odczyt źródeł publicznych zakończono 2026-07-02. Pierwotna rekonstrukcja nadal korzysta z lokalnego obrazu stanu faktycznego z 2026-06-21.

Dowody

Certyfikaty i hashe

Obraz źródłowy zapisuje kanoniczny .npcert, certificate_hash, export_hash, axiom_report_hash i werdykty sprawdzaczy.

Licencja

Apache-2.0 zweryfikowana

Apache-2.0 zweryfikowano dla npa, npa-std i npa-mathlib przez publiczne metadane licencji 2026-07-02.

Granica

NPA nie jest praktycznym zamiennikiem Lean ani Rocq. Przeglądarkowa symulacja inspekcji nie uruchamia samego NPA. Publiczne tagi, licencję i widoczność repozytoriów sprawdzono 2026-07-02 na potrzeby końcowego odczytu przed publikacją.

Granica zaufania

Przenoś przez granicę dowodową wyłącznie kanoniczny certyfikat.

Granica nie dotyczy tego, które narzędzie wygląda na zaawansowane. Dotyczy tego, który artefakt może stać się dowodem po niezależnym sprawdzeniu.

Parser, elaborator, taktyki, automatyzacja, wyszukiwanie twierdzeń, wtyczki, systemy AI, pliki źródłowe, pliki odtwarzania, indeksy twierdzeń, plany publikacji, stan CI, strony wydań i metadane rejestru pozostają po niezaufanej stronie kandydatów.

Przepływ dowodowy / symulacja objaśniająca

Pokaż dokładny przepływ od bajtów certyfikatu do dowodów weryfikacji.

Symulacja w przeglądarce nie uruchamia samego NPA, Rust, WASM ani rzeczywistych certyfikatów dowodów. Wizualizuje kolejność sprawdzania niezależnego od źródeł, którą muszą spełnić rzeczywiste artefakty.

Ścieżka dowodowa CLI

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

NPA / ślad audytu GOTOWE

01 Format certyfikatukanoniczne bajty .npcert / certyfikat możliwy do parsowania / kontrola formatu CZEKAJ
02 Hash certyfikatubajty certyfikatu / certificate_hash / deterministyczny skrót CZEKAJ
03 Werdykt jądracertyfikat / akceptacja albo odrzucenie / raport weryfikatora Rust CZEKAJ
04 Sprawdzacz referencyjnycertyfikat przypięty hashem / niezależna akceptacja albo odrzucenie / raport sprawdzacza niezależnego od źródeł CZEKAJ
05 Raport aksjomatówsprawdzony pakiet / axiom_report_hash / spis założeń CZEKAJ

Werdykt

Objaśniający przepływ nie został jeszcze uruchomiony.

Uruchom objaśnienie, aby oznaczyć kolejno ścieżkę sprawdzania niezależnego od źródeł.

Rejestr twierdzeń

Oddzielaj dowody, fakty zależne od czasu i twierdzenia o granicach.

Strona nie opiera się na luźnym tekście badawczym. Każde publiczne stwierdzenie jest powiązane z lokalnym obrazem stanu faktycznego, źródłem i działaniem przed publikacją.

Twierdzenie	Sformułowanie publiczne	Stan	Źródło	Działanie przed publikacją
CL-001	NPA stawia certyfikat na pierwszym miejscu: granicą podlegającą audytowi jest kanoniczny artefakt .npcert oraz otaczająca go ścieżka sprawdzania.	Zweryfikowane twierdzenie publiczne	S01 / 2026-07-02	Ponownie przejrzyj po zmianie README.
CL-002	Publiczna ponowna kontrola z 2026-07-02 wykazała, że najnowszy tag git repozytorium NPA to v0.2.0. Pliki README powiązanych pakietów nadal wskazują wersje przypisane do poszczególnych repozytoriów, dlatego sformułowania o wersjach pozostają ograniczone do danego repozytorium.	Zweryfikowana publiczna ponowna kontrola	S01 / S02 / 2026-07-02	Ogranicz sformułowanie o tagu do odpowiedniego repozytorium.
CL-003	Lokalny obraz stanu faktycznego zapisuje przypięcie łańcucha narzędzi Rust 1.95.0; nie jest ono używane jako twierdzenie marketingowe.	Zweryfikowane, zależne od czasu	S01 / 2026-07-02	Sprawdź ponownie, jeśli wyświetlana jest wersja łańcucha narzędzi.
CL-004	NPA nie jest praktycznym zamiennikiem Lean ani Rocq. Ta granica musi pozostać widoczna przy każdym porównaniu.	Zweryfikowane twierdzenie o granicy	S01 / S03 / S05 / 2026-07-02	Zachowaj to zastrzeżenie.
CL-005	npa-std i npa-mathlib są oddzielnymi publicznymi repozytoriami pakietów twierdzeń w organizacji finitefield-org.	Zweryfikowane twierdzenie publiczne	S01 / S02 / 2026-07-02	Ponownie sprawdź widoczność repozytoriów, jeśli publikacja się opóźni lub repozytoria się zmienią.
CL-006	Repozytoria npa, npa-std i npa-mathlib udostępniają licencję Apache-2.0 w swoich publicznych metadanych licencji.	Zweryfikowane twierdzenie publiczne	S01 / S02 / 2026-07-02	Ponownie sprawdź plik licencji przy dużym wydaniu.

Repozytoria i licencja

Wyraźnie pokaż kod, repozytoria pakietów i widoczność organizacji.

Łącza do repozytoriów wskazują publiczne źródła, ale nie gwarantują synchronizacji tej strony z najnowszym stanem GitHub.

4 wyświetlonych repozytoriów

finitefield-org

npa

Łańcuch narzędzi do wspomagania i weryfikacji dowodów, w którym certyfikat jest punktem wyjścia.

Licencja: Apache-2.0 zweryfikowano na podstawie pliku licencji 2026-07-02.
Weryfikacja: Najnowszy tag git: v0.2.0. Nie opublikowano najnowszej wersji GitHub. Bieżące odniesienie do łańcucha narzędzi w README: NPA_GIT_TAG=v0.2.0.

eksperymentalneRust / OCamlcertyfikat jako punkt wyjścia

Otwórz repozytorium

finitefield-org

npa-std

Repozytorium standardowego pakietu twierdzeń dla źródeł dowodów NPA.

Licencja: Apache-2.0 zweryfikowano na podstawie pliku licencji 2026-07-02.
Weryfikacja: Najnowszy tag git i wydanie GitHub: v0.1.0. Wersja metadanych pakietu w README: 0.1.0; przypięcie łańcucha narzędzi pakietu: NPA_GIT_TAG=v0.1.1.

eksperymentalnepakiet twierdzeńźródło dowodu

Otwórz repozytorium

finitefield-org

npa-mathlib

Repozytorium badawcze biblioteki matematyki formalnej.

Licencja: Apache-2.0 zweryfikowano na podstawie pliku licencji 2026-07-02.
Weryfikacja: Najnowszy tag git: v0.1.30. Najnowsze wydanie GitHub: v0.1.9. Wersja metadanych pakietu w README: 0.2.1; przypięcie łańcucha narzędzi pakietu: NPA_GIT_TAG=v0.1.1.

badaniamatematyka formalnabiblioteka

Otwórz repozytorium

finitefield-org

Organizacja GitHub Finite Field

Publiczny obraz organizacji dla rodziny repozytoriów Lab.

Licencja: Obowiązują licencje właściwe dla repozytoriów
Weryfikacja: npa, npa-std i npa-mathlib są publiczne według ponownego odczytu API GitHub z 2026-07-02.

indeks publicznymigawka widocznościźródło

Otwórz organizację

Repozytoria GitHub są źródłem publicznego stanu kodu. Licencję, bieżące tagi, publiczną widoczność i sformułowania o wydaniach sprawdzono 2026-07-02 w końcowym odczycie M10-T14.

Kontrola ekosystemu dowodowego

Wyjaśnij role przed porównaniem narzędzi dowodowych.

To tabela ról, a nie ranking. Lean i Rocq pozostają referencyjnymi ekosystemami asystentów dowodzenia; NPA jest przedstawiane jako praca badawcza i wdrożeniowa skupiona na certyfikatach.

Element	Lean	Rocq	NPA
Pozycja	Język programowania o otwartym kodzie i asystent dowodzenia.	Interaktywny system dowodzenia twierdzeń o długiej historii badawczej.	Repozytorium badań i implementacji sprawdzania skupionego na certyfikatach.
Typowe zastosowanie	Matematyka, weryfikacja oprogramowania i programowanie.	Matematyka, specyfikacje, weryfikacja programów i ekstrakcja.	Badania nad certyfikatami dowodów, niezależnym sprawdzaniem i małą zaufaną bazą.
Granica dowodowa	Jego własne zaufane jądro i ekosystem wyznaczają granicę sprawdzania.	Jego własne jądro i sprawdzone opracowania wyznaczają granicę sprawdzania.	Kanoniczny artefakt .npcert przechodzi z generowania do sprawdzania.
Ujęcie na tej stronie	Punkt odniesienia do nauki, porównań i interoperacyjności.	Punkt odniesienia do nauki, porównań i metod formalizacji.	Projekt badawczy Finite Field, nie obietnica produktu.
Granica	Nadal wymagana jest wiedza specjalistyczna.	Nadal wymagana jest wiedza specjalistyczna.	NPA nie jest obecnie praktycznym zamiennikiem Lean ani Rocq.

Oficjalna strona Lean Oficjalna strona Rocq Prover NPA GitHub

Źródła

Publikuj mapę źródeł obok interpretacji.

Źródła pokazano, aby czytelnik mógł rozpoznać, które twierdzenia pochodzą z publicznych repozytoriów, oficjalnych stron narzędzi dowodowych i kontekstu firmy.

S01

finitefield-org/npa

Główne źródło celu i modelu zaufania NPA, sformułowania bieżącego tagu v0.2.0, poleceń, układu repozytorium i licencji.

Otwórz źródło S02

Organizacja GitHub Finite Field

Główne źródło publicznej widoczności repozytoriów, najnowszych tagów git, stron wydań i obrazu rodziny repozytoriów Lab sprawdzonego 2026-07-02.

Otwórz źródło S03

Oficjalna strona Lean

Główne źródło publicznego pozycjonowania Lean, sprawdzone 2026-07-02.

Otwórz źródło S04

Dokumentacja języka Lean

Główne źródło kontekstu zależnej teorii typów i odniesienia do jądra, sprawdzone 2026-07-02.

Otwórz źródło S05

Oficjalna strona Rocq Prover

Główne źródło publicznego pozycjonowania Rocq, sprawdzone 2026-07-02.

Otwórz źródło S06

Strona firmowa FINITE FIELD

Źródło firmowe dla marki Finite Field i kontekstu biznesowego.

Otwórz źródło

FAQ

Stan NPA i granice weryfikacji.

Odpowiedzi podkreślają granicę zaufania, zanim czytelnik pomyli stronę badawczą z wdrożoną usługą asystenta dowodzenia.

Poznaj firmę

01 Czy ta strona stanowi gwarancję produktu?

Nie. NPA jest tu pokazane jako repozytorium badań i implementacji.

02 Czy NPA może zastąpić Lean lub Rocq?

Nie. NPA nie jest praktycznym zamiennikiem Lean ani Rocq.

03 Czy strona uruchamia rzeczywistą weryfikację NPA?

Nie. Symulacja w przeglądarce nie uruchamia samego NPA, Rust, WASM ani rzeczywistych certyfikatów dowodów.

04 Co jest tutaj uznawane za dowód?

Artefakt certyfikatu, deterministyczne hashe, wynik jądra/weryfikatora Rust, wynik sprawdzacza referencyjnego niezależnego od źródeł i raport aksjomatów stanowią dowody po stronie sprawdzania.

05 Które fakty wymagają ponownego sprawdzenia?

Aktualna wersja publiczna, widoczność repozytoriów, przypięcia łańcucha narzędzi, tekst licencji i sformułowania źródeł zostały ponownie sprawdzone 2026-07-02.

Od dyscypliny dowodowej do operacji

Stosuj tę samą dyscyplinę dowodową, gdy decyzja biznesowa musi być godna zaufania.

W systemach biznesowych użyteczną lekcją nie jest dodawanie dowodzenia twierdzeń wszędzie. Chodzi o ustalenie, co ludzie muszą generować, sprawdzać, rejestrować, poprawiać i zatwierdzać.

Sprawdź problem biznesowy Zobacz prototyp