Stav
Výskumný a implementačný repozitár
Repozitár GitHub je verejný, ale táto stránka opisuje výskumný a implementačný repozitár, nie nasadenú službu.
Späť do Matematického laboratória
NPA / Kontrola dôkazov s certifikátom na prvom mieste
NPA: ukážte hranicu dôkazov skôr, než výsledku začnete dôverovať.
Táto stránka rozvíja sekciu NPA z Matematického laboratória ako samostatnú stránku dôkazov: verejný stav, model dôvery, dôkazový postup, register tvrdení, repozitáre, zdroje a výslovné upozornenie, že nejde o náhradu za Lean ani Rocq.
- Stav
- Výskum a implementácia
- Uvádzané ako výskum a implementácia, nie ako produkčná záručná služba.
- Snímka
- 2026-07-02 / NPA v0.2.0
- Skontrolované najnovšie git tagy: npa v0.2.0, npa-std v0.1.0, npa-mathlib v0.1.30.
- Licencia
- Apache-2.0
- Apache-2.0 bolo pre npa, npa-std a npa-mathlib overené 2026-07-02.
Snímka verejných informácií a formulácie stránok boli skontrolované 2026-07-02.
Verejný stav
Rozsah stránky je dôkazová hranica, nie produktový sľub.
Každé tvrdenie je viazané na zdroj, dátum kontroly a hranicu publikovania. Stránka nemá naznačovať, že NPA je náhrada za zrelé dokazovacie asistenty.
Kontrola
2026-07-02
Spätné overenie verejných zdrojov bolo dokončené 2026-07-02. Pôvodná rekonštrukcia zdrojov stále používa lokálny pravdivostný snímok z 2026-06-21.
Dôkazy
Certifikáty a hashe
Zdrojový snímok zaznamenáva kanonické .npcert, certificate_hash, export_hash, axiom_report_hash a verdikty kontrolérov.
Licencia
Apache-2.0 overené
Apache-2.0 bolo overené pre npa, npa-std a npa-mathlib cez verejné metadáta LICENSE dňa 2026-07-02.
Hranica
NPA nie je praktickou náhradou za Lean ani Rocq. Distribuovaná kontrolná simulácia v prehliadači nespúšťa samotné NPA. Verejné tagy, licencia a viditeľnosť repozitára boli skontrolované 2026-07-02 pre záverečné spätné overenie pred publikovaním.
Hranica dôvery
Oddeľte generovanie kandidátov od kontrolnej strany.
Hranica nie je o tom, ktorý nástroj vyzerá sofistikovane. Ide o to, ktorý artefakt sa môže stať dôkazom po nezávislej kontrole.
Parser, elaborátor, taktiky, automatizácia, vyhľadávanie viet, pluginy, systémy AI, zdrojové súbory, replay súbory, indexy viet, plány publikovania, stav CI, stránky vydaní a metadáta registrácie zostávajú na nedôveryhodnej strane kandidátov.
Dôkazový postup / vysvetľujúca simulácia
Ukážte presný postup od bajtov certifikátu po kontrolné dôkazy.
Simulácia v prehliadači nespúšťa samotné NPA, Rust, WASM ani skutočné dôkazové certifikáty. Zobrazuje poradie kontroly bez zdrojových súborov, ktoré musia reálne artefakty splniť.
Cesta dôkazov v CLI
npa package verify-certs --root . --checker reference --json
NPA / auditná stopa
PRIPRAVENÉ
- 01 Formát certifikátukanonické bajty .npcert / parsovateľný certifikát / kontrola formátu ČAKÁ
- 02 Hash certifikátubajty certifikátu / certificate_hash / deterministický odtlačok ČAKÁ
- 03 Verdikt jadracertifikát / prijať alebo odmietnuť / správa verifikátora v Ruste ČAKÁ
- 04 Referenčný kontrolércertifikát pripnutý hashom / nezávislé prijatie alebo odmietnutie / správa kontroléra bez zdrojových súborov ČAKÁ
- 05 Správa o axiómachskontrolovaný balík / axiom_report_hash / inventár predpokladov ČAKÁ
Verdikt
Vysvetľujúci postup ešte nebol spustený.Spustite vysvetlenie a zobrazte kontrolnú cestu bez zdrojových súborov v správnom poradí.
Register tvrdení
Oddeľte dôkazy, časovo citlivé fakty a hraničné tvrdenia.
Stránka nestojí na voľnom výskumnom texte. Každé verejné tvrdenie je naviazané na lokálny pravdivostný snímok, zdroj a publikačný krok.
| Tvrdenie | Verejné znenie | Stav | Zdroj | Publikačný krok |
|---|---|---|---|---|
| CL-001 | NPA je navrhnuté s certifikátom na prvom mieste: auditovateľnou hranicou je kanonický artefakt .npcert a kontrolná cesta okolo neho. | Overené verejné tvrdenie | S01 / 2026-07-02 | Skontrolovať pri zmene README. |
| CL-002 | Verejná opätovná kontrola z 2026-07-02 zistila, že najnovší git tag repozitára NPA je v0.2.0. README súvisiacich balíkov stále uvádzajú piny špecifické pre repozitár, preto formulácia verzie zostáva obmedzená na konkrétny repozitár. | Overená verejná opätovná kontrola | S01 / S02 / 2026-07-02 | Ponechať formuláciu tagu viazanú na repozitár. |
| CL-003 | Lokálny pravdivostný snímok zaznamenáva pin nástrojového reťazca Rust 1.95.0; nepoužíva sa ako marketingové tvrdenie. | Overené, časovo citlivé | S01 / 2026-07-02 | Znovu skontrolovať, ak sa verzia nástrojového reťazca zobrazí verejne. |
| CL-004 | NPA nie je praktickou náhradou za Lean ani Rocq. Táto hranica musí zostať viditeľná pri každom porovnaní. | Overené hraničné tvrdenie | S01 / S03 / S05 / 2026-07-02 | Ponechať upozornenie. |
| CL-005 | npa-std a npa-mathlib sú samostatné verejné repozitáre balíkov teorém v organizácii finitefield-org. | Overené verejné tvrdenie | S01 / S02 / 2026-07-02 | Pri oneskorení publikácie alebo zmene repozitárov znovu overiť ich viditeľnosť. |
| CL-006 | Repozitáre npa, npa-std a npa-mathlib každý verejne uvádzajú licenciu Apache-2.0 cez metadáta LICENSE. | Overené verejné tvrdenie | S01 / S02 / 2026-07-02 | Pri veľkom vydaní znovu skontrolovať LICENSE. |
Repozitáre a licencia
Udržujte kód, balíkové repozitáre a viditeľnosť organizácie explicitné.
Odkazy na repozitáre sú verejné zdrojové ukazovatele, nie záruka, že aktuálna stránka je zosynchronizovaná s najnovším stavom na GitHube.
4 zobrazených repozitárov
finitefield-org
npa
Nástrojový reťazec na dôkazovú asistenciu a overovanie s certifikátom na prvom mieste.
- Licencia
- Apache-2.0 overené z LICENSE dňa 2026-07-02.
- Overenie
- Najnovší git tag: v0.2.0. Najnovšie vydanie na GitHube nie je publikované. Aktuálna referencia nástrojového reťazca v README: NPA_GIT_TAG=v0.2.0.
experimentálneRust / OCamlcertifikát na prvom mieste
Otvoriť repozitár
finitefield-org
npa-std
Repozitár štandardného balíka teorém pre zdroje dôkazov NPA.
- Licencia
- Apache-2.0 overené z LICENSE dňa 2026-07-02.
- Overenie
- Najnovší git tag a vydanie na GitHube: v0.1.0. Verzia v metadátach balíka README: 0.1.0; pin nástrojového reťazca balíka: NPA_GIT_TAG=v0.1.1.
experimentálnebalík teorémzdroj dôkazov
Otvoriť repozitár
finitefield-org
npa-mathlib
Výskumný repozitár knižnice formálnej matematiky.
- Licencia
- Apache-2.0 overené z LICENSE dňa 2026-07-02.
- Overenie
- Najnovší git tag: v0.1.30. Najnovšie vydanie na GitHube: v0.1.9. Verzia v metadátach balíka README: 0.2.1; pin nástrojového reťazca balíka: NPA_GIT_TAG=v0.1.1.
výskumformálna matematikaknižnica
Otvoriť repozitár
finitefield-org
Organizácia Finite Field na GitHube
Verejný snímok organizácie pre rodinu repozitárov Lab.
- Licencia
- Platia licencie konkrétnych repozitárov
- Overenie
- npa, npa-std a npa-mathlib sú podľa spätného čítania cez GitHub API z 2026-07-02 verejné.
verejný indexsnímok viditeľnostizdroj
Otvoriť organizáciu
Aktuálnemu vyhľadávaniu nezodpovedá žiadny repozitár.
Repozitáre na GitHube sú zdrojom verejného stavu kódu. Licencie, aktuálne tagy, verejná viditeľnosť a formulácie o vydaniach boli skontrolované 2026-07-02 ako záverečné spätné overenie M10-T14.
Ochrana ekosystému dôkazov
Pred porovnávaním dôkazových nástrojov ujasnite roly.
Toto je tabuľka rolí, nie rebríček. Lean a Rocq zostávajú referenčnými ekosystémami dôkazových asistentov; NPA je prezentované ako výskumná a implementačná práca zameraná na certifikáty.
| Položka | Lean | Rocq | NPA |
|---|---|---|---|
| Pozícia | Programovací jazyk a dôkazový asistent s otvoreným zdrojovým kódom. | Interaktívny dokazovač teorém s dlhou výskumnou históriou. | Výskumný a implementačný repozitár pre kontrolu s certifikátom na prvom mieste. |
| Typické použitie | Matematika, overovanie softvéru a programovanie. | Matematika, špecifikácie, overovanie programov a extrakcia. | Výskum dôkazových certifikátov, nezávislej kontroly a malej dôveryhodnej bázy. |
| Hranica dôkazov | Vlastné dôveryhodné jadro a ekosystém určujú kontrolnú hranicu. | Vlastné jadro a skontrolované vývoje určujú kontrolnú hranicu. | Kanonický artefakt .npcert prechádza z generovania do kontroly. |
| Ako s tým táto stránka pracuje | Referencia pre učenie, porovnávanie a interoperabilitu. | Referencia pre učenie, porovnávanie a metódy formalizácie. | Výskumný projekt Finite Field, nie produktový prísľub. |
| Hranica | Odborné znalosti sú stále potrebné. | Odborné znalosti sú stále potrebné. | NPA momentálne nie je praktickou náhradou za Lean ani Rocq. |
Zdroje
Zverejnite mapu zdrojov vedľa interpretácie.
Zdroje sú uvedené preto, aby čitateľ rozlíšil tvrdenia pochádzajúce z verejných repozitárov, oficiálnych stránok dôkazových nástrojov a kontextu spoločnosti.
S01
finitefield-org/npa
Primárny zdroj účelu NPA, modelu dôvery, formulácie aktuálneho tagu repozitára v0.2.0, príkazov, štruktúry repozitára a licencie.
Otvoriť zdroj S02Organizácia Finite Field na GitHube
Primárny zdroj verejnej viditeľnosti repozitárov, najnovších git tagov, stránok vydaní a snímky rodiny repozitárov Lab skontrolovanej 2026-07-02.
Otvoriť zdroj S03Oficiálna stránka Lean
Primárny zdroj verejného predstavenia Lean, skontrolovaný 2026-07-02.
Otvoriť zdroj S04Referencia jazyka Lean
Primárny zdroj kontextu závislostnej teórie typov a referencie jadra, skontrolovaný 2026-07-02.
Otvoriť zdroj S05Oficiálna stránka Rocq Prover
Primárny zdroj verejného predstavenia Rocq, skontrolovaný 2026-07-02.
Otvoriť zdroj S06Firemná stránka FINITE FIELD
Firemný zdroj pre značku Finite Field a obchodný kontext.
Otvoriť zdrojČasté otázky
Stav NPA a hranice overovania.
Odpovede zdôrazňujú hranicu dôvery skôr, než si čitateľ zamení výskumnú stránku s nasadenou službou dôkazového asistenta.
Prečítať si o spoločnosti01 Je táto stránka produktovou zárukou?
Nie. NPA je tu zobrazené ako výskumný a implementačný repozitár.
02 Môže NPA nahradiť Lean alebo Rocq?
Nie. NPA nie je praktickou náhradou za Lean ani Rocq.
03 Spúšťa stránka skutočné overovanie NPA?
Nie. Simulácia v prehliadači nespúšťa samotné NPA, Rust, WASM ani reálne dôkazové certifikáty.
04 Čo sa tu počíta ako dôkaz?
Dôkaz na strane kontroly tvorí certifikačný artefakt, deterministické hashe, výsledok jadra/verifikátora v Ruste, výsledok referenčného kontroléra bez zdrojových súborov a správa o axiómach.
05 Ktoré fakty treba znovu kontrolovať?
Aktuálna verejná verzia, viditeľnosť repozitárov, piny nástrojového reťazca, text licencie a formulácie zdrojov boli znovu skontrolované 2026-07-02.
Od dôkazovej disciplíny k prevádzke
Rovnakú dôkazovú disciplínu použite aj vtedy, keď treba dôverovať obchodnému rozhodnutiu.
Pri podnikových systémoch nie je užitočnou lekciou pridávať dokazovanie teorém všade. Ide o rozhodnutie, čo sa musí generovať, kontrolovať, logovať, opravovať a schvaľovať ľuďmi.