Stare publică
Depozit de cercetare și implementare
Depozitul GitHub este public, dar această pagină descrie un depozit de cercetare și implementare, nu un serviciu implementat în producție.
Înapoi la Math Lab
NPA / Verificarea demonstrațiilor centrată pe certificate
NPA: expuneți limita dovezilor de demonstrație înainte de a avea încredere într-un rezultat.
Această pagină reconstruiește secțiunea NPA din Math Lab ca pagină independentă de dovezi: stare publică, model de încredere, flux de demonstrație, registru de afirmații, depozite, surse și formulare explicită că nu este un înlocuitor.
- Stare publică
- Depozit de cercetare
- Prezentat ca cercetare și implementare, nu ca serviciu de asigurare pentru producție.
- Reverificare publică
- 2026-07-02 / NPA v0.2.0
- Cele mai recente taguri git verificate: npa v0.2.0, npa-std v0.1.0, npa-mathlib v0.1.30.
- Licență
- Apache-2.0
- Apache-2.0 a fost verificată pentru npa, npa-std și npa-mathlib la 2026-07-02.
Reverificare publică: 2026-07-02. Cea mai recentă etichetă git a depozitului NPA este v0.2.0; npa-std este v0.1.0; npa-mathlib este v0.1.30. Fixările din README-urile pachetelor sunt prezentate ca context specific depozitului și nu sunt aplatizate într-o singură afirmație de versiune NPA.
Stare publică
Precizați ce este public, ce este dovadă și când a fost reverificat.
Această pagină face vizibilă baza paginii: un instantaneu local al adevărului, o sursă de depozit public și data citirii finale înainte de lansare.
Reverificare publică
2026-07-02
Citirea surselor publice a fost finalizată la 2026-07-02. Reconstrucția sursei originale folosește în continuare instantaneul local al adevărului din 2026-06-21.
Dovezi
Certificate și hash-uri
Instantaneul sursei înregistrează .npcert canonic, certificate_hash, export_hash, axiom_report_hash și verdictele verificatoarelor.
Licență
Apache-2.0 verificată
Apache-2.0 a fost verificată pentru npa, npa-std și npa-mathlib prin metadatele publice LICENSE la 2026-07-02.
Limită
NPA nu este un înlocuitor practic pentru Lean sau Rocq. Simularea distribuită de inspectare din browser nu rulează NPA. Tagurile publice, licența și vizibilitatea depozitelor au fost verificate la 2026-07-02 pentru citirea finală înainte de publicare.
Limită de încredere
Mutați peste limita dovezilor doar un certificat canonic.
Limita nu ține de ce instrument pare sofisticat. Ține de artefactul căruia i se permite să devină dovadă după verificare independentă.
Analizorul sintactic, elaboratorul, tacticile, automatizarea, căutarea de teoreme, extensiile, sistemele AI, fișierele sursă, fișierele de reluare, indicii de teoreme, planurile de publicare, starea CI, paginile de lansare și metadatele de registru rămân pe partea neverificată a candidaților.
Flux de demonstrație / simulare explicativă
Arătați fluxul exact de la octeții certificatului la dovezile de verificare.
Simularea din browser nu rulează NPA, Rust, WASM sau certificate reale de demonstrație. Ea vizualizează ordinea verificării fără sursă pe care artefactele reale trebuie să o satisfacă.
Traseu CLI pentru dovezi
npa package verify-certs --root . --checker reference --json
NPA / urmă de audit
GATA
- 01 Formatul certificatuluiocteți canonici .npcert / certificat parsabil / verificare de format AȘTEAPTĂ
- 02 Hash-ul certificatuluiocteții certificatului / certificate_hash / digest determinist AȘTEAPTĂ
- 03 Verdictul nucleuluicertificat / acceptare sau respingere / raportul verificatorului Rust AȘTEAPTĂ
- 04 Verificator de referințăcertificat fixat prin hash / acceptare sau respingere independentă / raportul verificatorului fără sursă AȘTEAPTĂ
- 05 Raport de axiomepachet verificat / axiom_report_hash / inventar de ipoteze AȘTEAPTĂ
Verdict
Fluxul explicativ nu a fost rulat încă.Rulați explicația pentru a marca în ordine traseul de verificare fără sursă.
Registru de afirmații
Separați dovezile, faptele sensibile la timp și afirmațiile de limită.
Pagina nu depinde de texte de cercetare neancorate. Fiecare afirmație publică este legată de un instantaneu local al adevărului, o sursă și o acțiune de publicare.
| Afirmație | Formulare publică | Stare | Sursă | Acțiune de publicare |
|---|---|---|---|---|
| CL-001 | NPA este centrat pe certificate: limita auditabilă este artefactul canonic .npcert și traseul de verificare din jurul lui. | Afirmație publică verificată | S01 / 2026-07-02 | Revizuiți când README-ul se schimbă. |
| CL-002 | Reverificarea publică din 2026-07-02 a găsit cea mai recentă etichetă git a depozitului NPA la v0.2.0. README-urile pachetelor asociate indică în continuare versiuni fixate specifice fiecărui depozit, deci formularea despre versiuni rămâne limitată pe depozit. | Reverificare publică validată | S01 / S02 / 2026-07-02 | Păstrați formularea tagurilor limitată pe depozit. |
| CL-003 | Instantaneul local al adevărului înregistrează o fixare a lanțului de instrumente Rust 1.95.0; aceasta nu este folosită ca afirmație de marketing. | Verificat, sensibil la timp | S01 / 2026-07-02 | Reverificați dacă versiunea lanțului de instrumente este afișată. |
| CL-004 | NPA nu este un înlocuitor practic pentru Lean sau Rocq. Această limită trebuie să rămână vizibilă lângă orice comparație. | Afirmație de limită verificată | S01 / S03 / S05 / 2026-07-02 | Păstrați avertismentul. |
| CL-005 | npa-std și npa-mathlib sunt depozite publice separate de pachete de teoreme în organizația finitefield-org. | Afirmație publică verificată | S01 / S02 / 2026-07-02 | Reverificați vizibilitatea depozitelor dacă publicarea este amânată sau depozitele se schimbă. |
| CL-006 | Depozitele npa, npa-std și npa-mathlib expun fiecare licențierea Apache-2.0 prin metadatele publice LICENSE. | Afirmație publică verificată | S01 / S02 / 2026-07-02 | Reverificați LICENSE la o lansare majoră. |
Depozite și licență
Păstrați explicite codul, depozitele de pachete și vizibilitatea organizației.
Linkurile către depozite sunt trimiteri la surse publice, nu garanții că pagina curentă este sincronizată cu cea mai recentă stare GitHub.
4 depozite afișate
finitefield-org
npa
Lanț de instrumente pentru asistență și verificare a demonstrațiilor centrat pe certificate.
- Licență
- Apache-2.0 verificată din LICENSE la 2026-07-02.
- Verificare
- Cea mai recentă etichetă git: v0.2.0. Nu este publicată nicio lansare GitHub recentă. Referința curentă a lanțului de instrumente din README: NPA_GIT_TAG=v0.2.0.
experimentalăRust / OCamlcentrat pe certificate
Deschideți depozitul
finitefield-org
npa-std
Depozit standard de pachete de teoreme pentru sursele de demonstrații NPA.
- Licență
- Apache-2.0 verificată din LICENSE la 2026-07-02.
- Verificare
- Cea mai recentă etichetă git și lansare GitHub: v0.1.0. Versiunea metadatelor pachetului din README: 0.1.0; fixarea lanțului de instrumente al pachetului: NPA_GIT_TAG=v0.1.1.
experimentalăpachet de teoremesursă de demonstrații
Deschideți depozitul
finitefield-org
npa-mathlib
Depozit de cercetare pentru bibliotecă de matematică formală.
- Licență
- Apache-2.0 verificată din LICENSE la 2026-07-02.
- Verificare
- Cea mai recentă etichetă git: v0.1.30. Cea mai recentă lansare GitHub: v0.1.9. Versiunea metadatelor pachetului din README: 0.2.1; fixarea lanțului de instrumente al pachetului: NPA_GIT_TAG=v0.1.1.
cercetarematematică formalăbibliotecă
Deschideți depozitul
finitefield-org
Organizația GitHub Finite Field
Instantaneu public al organizației pentru familia de depozite Lab.
- Licență
- Se aplică licențe specifice fiecărui depozit
- Verificare
- npa, npa-std și npa-mathlib sunt publice conform citirii API GitHub din 2026-07-02.
index publicinstantaneu de vizibilitatesursă
Deschideți organizația
Niciun depozit nu se potrivește căutării curente.
Depozitele GitHub sunt sursa pentru starea publică a codului. Licența, etichetele curente, vizibilitatea publică și formularea despre lansări au fost verificate la 2026-07-02 ca citire finală M10-T14.
Gardă pentru ecosistemul de demonstrații
Clarificați rolurile înainte de a compara instrumentele de demonstrație.
Acesta este un tabel de roluri, nu un clasament. Lean și Rocq rămân ecosisteme de referință pentru asistenți de demonstrație; NPA este prezentat ca activitate de cercetare și implementare centrată pe certificate.
| Element | Lean | Rocq | NPA |
|---|---|---|---|
| Poziție | Limbaj de programare cu sursă deschisă și asistent de demonstrație. | Doveditor interactiv de teoreme cu o istorie lungă de cercetare. | Depozit de cercetare și implementare pentru verificare centrată pe certificate. |
| Utilizare tipică | Matematică, verificare software și programare. | Matematică, specificații, verificarea programelor și extracție. | Cercetare privind certificatele de demonstrație, verificarea independentă și o bază mică de încredere. |
| Limită a dovezilor | Propriul nucleu de încredere și ecosistemul definesc limita verificării. | Propriul nucleu și dezvoltările verificate definesc limita verificării. | Artefactul canonic .npcert trece de la generare la verificare. |
| Cum îl tratează această pagină | Referință pentru învățare, comparație și interoperabilitate. | Referință pentru învățare, comparație și metode de formalizare. | Proiect de cercetare Finite Field, nu o promisiune de produs. |
| Limită | Cunoștințele de specialitate rămân necesare. | Cunoștințele de specialitate rămân necesare. | În prezent, NPA nu este un înlocuitor practic pentru Lean sau Rocq. |
Surse
Publicați harta surselor lângă interpretare.
Sursele sunt afișate pentru ca cititorul să poată vedea ce afirmații provin din depozite publice, site-uri oficiale ale instrumentelor de demonstrație și contextul companiei.
S01
finitefield-org/npa
Sursă primară pentru scopul NPA, modelul de încredere, formularea tagului curent v0.2.0 al depozitului, comenzi, structura depozitului și licență.
Sursă deschisă S02Organizația GitHub Finite Field
Sursă primară pentru vizibilitatea depozitelor publice, cele mai recente etichete git, pagini de lansare și instantaneul familiei de depozite Lab verificat la 2026-07-02.
Sursă deschisă S03Site oficial Lean
Sursă primară pentru poziționarea publică a Lean, verificată la 2026-07-02.
Sursă deschisă S04Referința limbajului Lean
Sursă primară pentru teoria tipurilor dependente și contextul de referință al nucleului, verificată la 2026-07-02.
Sursă deschisă S05Site oficial Rocq Prover
Sursă primară pentru poziționarea publică a Rocq, verificată la 2026-07-02.
Sursă deschisă S06Site-ul companiei FINITE FIELD
Sursă de companie pentru marca Finite Field și contextul de afaceri.
Sursă deschisăÎntrebări frecvente
Starea NPA și limitele verificării.
Răspunsurile subliniază limita de încredere înainte ca cititorii să confunde o pagină de cercetare cu un serviciu de asistență pentru demonstrații aflat în producție.
Citiți despre companie01 Este această pagină o garanție de produs?
Nu. NPA este prezentat aici ca depozit de cercetare și implementare.
02 Poate NPA să înlocuiască Lean sau Rocq?
Nu. NPA nu este un înlocuitor practic pentru Lean sau Rocq.
03 Pagina rulează verificare NPA reală?
Nu. Simularea din browser nu rulează NPA, Rust, WASM sau certificate reale de demonstrație.
04 Ce contează aici ca dovadă?
Artefactul certificatului, hash-urile deterministe, rezultatul nucleului/verificatorului Rust, rezultatul verificatorului de referință fără sursă și raportul de axiome formează dovada de pe partea de verificare.
05 Ce fapte trebuie reverificate?
Versiunea publică actuală, vizibilitatea depozitelor, fixările lanțului de instrumente, textul licenței și formularea sursei au fost reverificate la 2026-07-02.
De la disciplina demonstrațiilor la operațiuni
Folosiți aceeași disciplină a dovezilor când o decizie de afaceri trebuie să fie de încredere.
Pentru sistemele de afaceri, lecția utilă nu este să adăugăm demonstrarea teoremelor peste tot. Este să decidem ce trebuie generat, verificat, jurnalizat, corectat și aprobat de oameni.