NPA / ověřování důkazů s certifikátem na prvním místě

NPA: před důvěrou ve výsledek odkryjte hranici důkazů.

Tato stránka rekonstruuje oddíl NPA z Math Lab jako samostatnou stránku důkazů: veřejný stav, model důvěry, důkazní postup, registr tvrzení, repozitáře, zdroje a výslovné znění, že NPA není náhradou.

Prozkoumat hranici důvěry Otevřít repozitář GitHub

Veřejný stav: Výzkumný repozitář; Prezentováno jako výzkum a implementace, nikoli jako služba provozního zajištění.
Veřejná opakovaná kontrola: 2026-07-02 / NPA v0.2.0; Zkontrolované nejnovější git tagy: npa v0.2.0, npa-std v0.1.0, npa-mathlib v0.1.30.
Licence: Apache-2.0; Apache-2.0 byla pro npa, npa-std a npa-mathlib ověřena 2. 7. 2026.

Veřejná opakovaná kontrola: 2. 7. 2026. Nejnovější git tag repozitáře NPA je v0.2.0; npa-std je v0.1.0; npa-mathlib je v0.1.30. Vazby v README balíčků jsou uvedeny jako kontext specifický pro repozitář a nejsou sloučeny do jediného tvrzení o verzi NPA.

Náhled stránky důkazů NPA zobrazující kontrolu certifikátu a prozkoumání hranice důvěry — Vizualizace je statickým náhledem výsledku kontroly certifikátu a vysvětlení hranice důvěry. Nejde o živou stopu NPA.

Veřejný stav

Uveďte, co je veřejné, co je důkaz a kdy proběhla opakovaná kontrola.

Tato stránka zviditelňuje svůj základ: lokální snímek ověřených skutečností, veřejný zdroj v repozitáři a datum závěrečné kontroly před spuštěním.

Veřejný stav

Výzkumný a implementační repozitář

Repozitář GitHub je veřejný, tato stránka však popisuje výzkumný a implementační repozitář, nikoli nasazenou službu.

Veřejná opakovaná kontrola

2026-07-02

Kontrola veřejných zdrojů byla dokončena 2. 7. 2026. Původní rekonstrukce zdrojů stále používá lokální snímek ověřených skutečností z 21. 6. 2026.

Důkazy

Certifikáty a hashe

Snímek zdrojů zaznamenává kanonický .npcert, certificate_hash, export_hash, axiom_report_hash a verdikty ověřovačů.

Licence

Apache-2.0 ověřena

Apache-2.0 byla pro npa, npa-std a npa-mathlib ověřena prostřednictvím veřejných metadat LICENSE dne 2. 7. 2026.

Hranice

NPA není praktickou náhradou za Lean ani Rocq. Distribuovaná simulace kontroly v prohlížeči nespouští samotné NPA. Veřejné tagy, licence a viditelnost repozitářů byly zkontrolovány 2. 7. 2026 pro závěrečnou kontrolu před zveřejněním.

Hranice důvěry

Přes hranici důkazů přenášejte pouze kanonický certifikát.

Hranice neurčuje, který nástroj působí sofistikovaně. Určuje, kterému artefaktu je po nezávislém ověření dovoleno stát se důkazem.

Parser, elaborátor, taktiky, automatizace, vyhledávání teorémů, pluginy, systémy AI, zdrojové soubory, soubory pro opakování, indexy teorémů, publikační plány, stav CI, stránky vydání a metadata registru zůstávají na nedůvěryhodné straně kandidátů.

Důkazní postup / vysvětlující simulace

Ukažte přesný postup od bajtů certifikátu k důkazům z ověřování.

Simulace v prohlížeči nespouští samotné NPA, Rust, WASM ani skutečné certifikáty důkazů. Znázorňuje pořadí ověřování bez zdrojového kódu, které musí skutečné artefakty splnit.

Cesta důkazů přes CLI

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

NPA / auditní stopa PŘIPRAVENO

01 Formát certifikátukanonické bajty .npcert / parsovatelný certifikát / kontrola formátu ČEKÁ
02 Hash certifikátubajty certifikátu / certificate_hash / deterministický otisk ČEKÁ
03 Verdikt jádracertifikát / přijmout nebo odmítnout / zpráva ověřovače v Rustu ČEKÁ
04 Referenční ověřovačcertifikát ukotvený hashem / nezávislé přijetí nebo odmítnutí / zpráva ověřovače bez zdrojového kódu ČEKÁ
05 Zpráva o axiomechzkontrolovaný balíček / axiom_report_hash / seznam předpokladů ČEKÁ

Verdikt

Vysvětlující postup ještě nebyl spuštěn.

Spusťte vysvětlení, aby se ověřovací cesta bez zdrojového kódu označila ve správném pořadí.

Registr tvrzení

Oddělujte důkazy, časově citlivé skutečnosti a tvrzení o hranicích.

Stránka se neopírá o volný výzkumný text. Každé veřejné sdělení je navázáno na lokální snímek ověřených skutečností, zdroj a krok před zveřejněním.

Tvrzení	Veřejné znění	Stav	Zdroj	Krok před zveřejněním
CL-001	NPA staví certifikát na první místo: auditovatelnou hranici tvoří kanonický artefakt .npcert a ověřovací cesta kolem něj.	Ověřené veřejné tvrzení	S01 / 2026-07-02	Při změně README tvrzení znovu posuďte.
CL-002	Veřejná opakovaná kontrola z 2. 7. 2026 zjistila, že nejnovější git tag repozitáře NPA je v0.2.0. Související soubory README balíčků stále uvádějí vazby specifické pro jednotlivé repozitáře, proto znění o verzích zůstává omezené na konkrétní repozitář.	Ověřeno veřejnou opakovanou kontrolou	S01 / S02 / 2026-07-02	Znění o tagu ponechte v rozsahu konkrétního repozitáře.
CL-003	Lokální snímek ověřených skutečností zaznamenává vazbu na sadu nástrojů Rust 1.95.0; nepoužívá se jako marketingové tvrzení.	Ověřeno, časově citlivé	S01 / 2026-07-02	Pokud se verze sady nástrojů zobrazuje, znovu ji ověřte.
CL-004	NPA není praktickou náhradou za Lean ani Rocq. Tato hranice musí zůstat viditelná u každého srovnání.	Ověřené tvrzení o hranici	S01 / S03 / S05 / 2026-07-02	Zachovejte toto upozornění.
CL-005	npa-std a npa-mathlib jsou samostatné veřejné repozitáře balíčků teorémů v organizaci finitefield-org.	Ověřené veřejné tvrzení	S01 / S02 / 2026-07-02	Pokud se zveřejnění opozdí nebo se repozitáře změní, znovu ověřte jejich viditelnost.
CL-006	Repozitáře npa, npa-std a npa-mathlib zveřejňují licenci Apache-2.0 prostřednictvím svých veřejných metadat LICENSE.	Ověřené veřejné tvrzení	S01 / S02 / 2026-07-02	Při hlavním vydání znovu zkontrolujte LICENSE.

Repozitáře a licence

Udržujte kód, repozitáře balíčků a viditelnost organizace výslovné.

Odkazy na repozitáře ukazují veřejné zdroje, ale nezaručují, že tato stránka vždy odpovídá nejnovějšímu stavu na GitHubu.

4 zobrazené repozitáře

finitefield-org

npa

Sada nástrojů pro asistované vytváření a ověřování důkazů s certifikátem na prvním místě.

Licence: Apache-2.0 ověřena ze souboru LICENSE dne 2. 7. 2026.
Ověření: Nejnovější git tag: v0.2.0. Není zveřejněno žádné nejnovější vydání GitHub. Aktuální reference sady nástrojů v README: NPA_GIT_TAG=v0.2.0.

experimentálníRust / OCamlcertifikát na prvním místě

Otevřít repozitář

finitefield-org

npa-std

Repozitář standardního balíčku teorémů pro zdroje důkazů NPA.

Licence: Apache-2.0 ověřena ze souboru LICENSE dne 2. 7. 2026.
Ověření: Nejnovější git tag a vydání GitHub: v0.1.0. Verze metadat balíčku v README: 0.1.0; vazba sady nástrojů balíčku: NPA_GIT_TAG=v0.1.1.

experimentálníbalíček teorémůzdroj důkazů

Otevřít repozitář

finitefield-org

npa-mathlib

Výzkumný repozitář knihovny formální matematiky.

Licence: Apache-2.0 ověřena ze souboru LICENSE dne 2. 7. 2026.
Ověření: Nejnovější git tag: v0.1.30. Nejnovější vydání GitHub: v0.1.9. Verze metadat balíčku v README: 0.2.1; vazba sady nástrojů balíčku: NPA_GIT_TAG=v0.1.1.

výzkumformální matematikaknihovna

Otevřít repozitář

finitefield-org

GitHub organizace Finite Field

Veřejný snímek organizace pro rodinu repozitářů Lab.

Licence: Platí licence konkrétních repozitářů
Ověření: npa, npa-std a npa-mathlib jsou podle opakované kontroly přes GitHub API z 2. 7. 2026 veřejné.

veřejný indexsnímek viditelnostizdroj

Otevřít organizaci

Zdrojem veřejného stavu kódu jsou repozitáře GitHub. Licence, aktuální tagy, veřejná viditelnost a znění o vydáních byly zkontrolovány 2. 7. 2026 při závěrečné kontrole M10-T14.

Kontrola ekosystému důkazů

Před srovnáváním důkazních nástrojů vyjasněte jejich role.

Toto je tabulka rolí, nikoli žebříček. Lean a Rocq zůstávají referenčními ekosystémy asistentů důkazů; NPA je představen jako výzkumná a implementační práce zaměřená na certifikáty.

Položka	Lean	Rocq	NPA
Postavení	Programovací jazyk s otevřeným zdrojovým kódem a asistent důkazů.	Interaktivní dokazovač teorémů s dlouhou výzkumnou historií.	Výzkumný a implementační repozitář pro ověřování s certifikátem na prvním místě.
Typické použití	Matematika, ověřování softwaru a programování.	Matematika, specifikace, ověřování programů a extrakce.	Výzkum certifikátů důkazů, nezávislého ověřování a malé důvěryhodné základny.
Hranice důkazů	Hranici ověřování vymezuje jeho vlastní důvěryhodné jádro a ekosystém.	Hranici ověřování vymezuje jeho vlastní jádro a ověřené vývoje.	Kanonický artefakt .npcert přechází z generování do ověřování.
Jak jej tato stránka pojímá	Reference pro výuku, srovnávání a interoperabilitu.	Reference pro výuku, srovnávání a metody formalizace.	Výzkumný projekt Finite Field, nikoli produktový příslib.
Hranice	Nadále jsou nutné odborné znalosti.	Nadále jsou nutné odborné znalosti.	NPA v současnosti není praktickou náhradou za Lean ani Rocq.

Oficiální web Lean Oficiální web Rocq Prover NPA na GitHubu

Zdroje

Publikujte mapu zdrojů společně s interpretací.

Zdroje jsou uvedeny, aby čtenář poznal, která tvrzení pocházejí z veřejných repozitářů, oficiálních webů důkazních nástrojů a firemního kontextu.

S01

finitefield-org/npa

Primární zdroj pro účel a model důvěry NPA, znění o aktuálním tagu repozitáře v0.2.0, příkazy, uspořádání repozitáře a licenci.

Otevřít zdroj S02

GitHub organizace Finite Field

Primární zdroj pro veřejnou viditelnost repozitářů, nejnovější git tagy, stránky vydání a snímek rodiny repozitářů Lab zkontrolovaný 2. 7. 2026.

Otevřít zdroj S03

Oficiální web Lean

Primární zdroj pro veřejné postavení Lean, zkontrolovaný 2. 7. 2026.

Otevřít zdroj S04

Referenční příručka jazyka Lean

Primární zdroj pro kontext závislé teorie typů a referenčního jádra, zkontrolovaný 2. 7. 2026.

Otevřít zdroj S05

Oficiální web Rocq Prover

Primární zdroj pro veřejné postavení Rocq, zkontrolovaný 2. 7. 2026.

Otevřít zdroj S06

Firemní web FINITE FIELD

Firemní zdroj pro značku Finite Field a podnikový kontext.

Otevřít zdroj

Časté otázky

Stav NPA a hranice ověřování.

Odpovědi zdůrazňují hranici důvěry dříve, než si čtenáři spletou výzkumnou stránku s nasazenou službou asistenta důkazů.

Informace o společnosti

01 Je tato stránka zárukou produktu?

Ne. NPA je zde představen jako výzkumný a implementační repozitář.

02 Může NPA nahradit Lean nebo Rocq?

Ne. NPA není praktickou náhradou za Lean ani Rocq.

03 Spouští stránka skutečné ověřování NPA?

Ne. Simulace v prohlížeči nespouští samotné NPA, Rust, WASM ani skutečné certifikáty důkazů.

04 Co se zde považuje za důkaz?

Certifikační artefakt, deterministické hashe, výsledek jádra a ověřovače v Rustu, výsledek referenčního ověřovače bez zdrojového kódu a zpráva o axiomech společně tvoří důkazy na straně ověřování.

05 Které skutečnosti vyžadují novou kontrolu?

Aktuální veřejná verze, viditelnost repozitářů, vazby sady nástrojů, text licence a znění zdrojů byly znovu ověřeny 2. 7. 2026.

Od důkazní disciplíny k provozu

Stejnou práci s důkazy použijte i tam, kde musí být podnikové rozhodnutí důvěryhodné.

U podnikových systémů není hlavním poučením přidat dokazování teorémů všude. Důležité je určit, co se má generovat, kontrolovat, zaznamenat, opravit a nakonec schválit člověkem.

Prověřit provozní problém Zobrazit prototyp