Vieša būsena
Tyrimų ir įgyvendinimo repozitorija
GitHub repozitorija vieša, bet šis puslapis aprašo tyrimų ir įgyvendinimo repozitoriją, o ne įdiegtą paslaugą.
Grįžti į Math Lab
NPA / Nuo sertifikato pradedamas įrodymų tikrinimas
NPA: prieš pasitikėdami rezultatu parodykite įrodymų ribą.
Šis puslapis Math Lab NPA skyrių perkuria kaip savarankišką įrodymų puslapį: vieša būsena, pasitikėjimo modelis, įrodymo eiga, teiginių registras, repozitorijos, šaltiniai ir aiški formuluotė, kad tai nėra Lean ar Rocq pakaitalas.
- Vieša būsena
- Tyrimų repozitorija
- Rodoma kaip tyrimų ir įgyvendinimo darbas, o ne kaip gamybinio užtikrinimo paslauga.
- Vieša pakartotinė patikra
- 2026-07-02 / NPA v0.2.0
- Patikrintos naujausios git žymos: npa v0.2.0, npa-std v0.1.0, npa-mathlib v0.1.30.
- Licencija
- Apache-2.0
- Apache-2.0 2026-07-02 patikrinta npa, npa-std ir npa-mathlib repozitorijoms.
Vieša pakartotinė patikra: 2026-07-02. Naujausia NPA repozitorijos git žyma yra v0.2.0; npa-std - v0.1.0; npa-mathlib - v0.1.30. Paketų README nurodytos fiksuotos versijos rodomos kaip konkrečios repozitorijos kontekstas ir nesuplakamos į vieną NPA versijos teiginį.
Vieša būsena
Nurodykite, kas vieša, kas yra įrodymas ir kada tai pakartotinai patikrinta.
Šis puslapis aiškiai parodo savo pagrindą: vietinę tiesos momentinę kopiją, viešą repozitorijos šaltinį ir galutinio patikrinimo prieš publikavimą datą.
Vieša pakartotinė patikra
2026-07-02
Viešųjų šaltinių patikra baigta 2026-07-02. Pirminė šaltinio rekonstrukcija vis dar remiasi 2026-06-21 vietine tiesos momentine kopija.
Įrodymai
Sertifikatai ir maišos
Šaltinio momentinė kopija fiksuoja kanoninį .npcert, certificate_hash, export_hash, axiom_report_hash ir tikrintuvų verdiktus.
Licencija
Apache-2.0 patikrinta
Apache-2.0 2026-07-02 patikrinta npa, npa-std ir npa-mathlib pagal viešus LICENSE metaduomenis.
Riba
NPA nėra praktinis Lean ar Rocq pakaitalas. Ši naršyklės tikrinimo simuliacija nevykdo paties NPA. Viešos žymos, licencija ir repozitorijų matomumas galutiniam patikrinimui prieš publikavimą patikrinti 2026-07-02.
Pasitikėjimo riba
Per įrodymų ribą perkelkite tik kanoninį sertifikatą.
Riba nėra apie tai, kuris įrankis atrodo sudėtingas. Ji nusako, kuriam artefaktui po nepriklausomo tikrinimo leidžiama tapti įrodymu.
Parseris, elaboratorius, taktikos, automatizavimas, teoremų paieška, įskiepiai, DI sistemos, šaltinio failai, replay failai, teoremų indeksai, publikavimo planai, CI būsena, leidimų puslapiai ir registro metaduomenys lieka nepatikimoje kandidatų pusėje.
Įrodymo eiga / paaiškinamoji simuliacija
Parodykite tikslų kelią nuo sertifikato baitų iki tikrinimo įrodymų.
Naršyklės simuliacija nevykdo paties NPA, Rust, WASM ar tikrų įrodymo sertifikatų. Ji parodo tikrinimo be šaltinių tvarką, kurią turi tenkinti tikri artefaktai.
CLI įrodymų kelias
npa package verify-certs --root . --checker reference --json
NPA / audito pėdsakas
PARENGTA
- 01 Sertifikato formataskanoniniai .npcert baitai / perskaitomas sertifikatas / formato patikra LAUKIA
- 02 Sertifikato maišasertifikato baitai / certificate_hash / deterministinė santrauka LAUKIA
- 03 Branduolio verdiktassertifikatas / priimti arba atmesti / Rust tikrintuvo ataskaita LAUKIA
- 04 Etaloninis tikrintuvasmaiša užfiksuotas sertifikatas / nepriklausomai priimti arba atmesti / be šaltinio veikianti tikrintuvo ataskaita LAUKIA
- 05 Aksiomų ataskaitapatikrintas paketas / axiom_report_hash / prielaidų inventorius LAUKIA
Verdiktas
Paaiškinamoji eiga dar nepaleista.Paleiskite paaiškinimą, kad pažymėtumėte tikrinimo be šaltinių kelią iš eilės.
Teiginių registras
Atskirkite įrodymus, laiko atžvilgiu jautrius faktus ir ribų teiginius.
Puslapis nesiremia laisvu tyrimų tekstu. Kiekvienas viešas teiginys susietas su vietine tiesos momentine kopija, šaltiniu ir publikavimo veiksmu.
| Teiginys | Vieša formuluotė | Būsena | Šaltinis | Publikavimo veiksmas |
|---|---|---|---|---|
| CL-001 | NPA prasideda nuo sertifikato: audituojama riba yra kanoninis .npcert artefaktas ir jį supantis tikrinimo kelias. | Patikrintas viešas teiginys | S01 / 2026-07-02 | Peržiūrėti pasikeitus README. |
| CL-002 | 2026-07-02 vieša pakartotinė patikra parodė, kad naujausia NPA repozitorijos git žyma yra v0.2.0. Susijusių paketų README vis dar rodo repozitorijoms būdingas fiksuotas versijas, todėl versijos formuluotė lieka apribota repozitorija. | Patikrinta vieša pakartotinė patikra | S01 / S02 / 2026-07-02 | Žymų formuluotę laikyti apribotą repozitorija. |
| CL-003 | Vietinė tiesos momentinė kopija fiksuoja Rust 1.95.0 įrankių grandinės versiją; tai nenaudojama kaip rinkodaros teiginys. | Patikrinta, jautru laikui | S01 / 2026-07-02 | Pakartotinai patikrinti, jei rodoma įrankių grandinės versija. |
| CL-004 | NPA nėra praktinis Lean ar Rocq pakaitalas. Ši riba turi likti matoma šalia bet kokio palyginimo. | Patikrintas ribos teiginys | S01 / S03 / S05 / 2026-07-02 | Išlaikyti atsakomybės ribojimo pastabą. |
| CL-005 | npa-std ir npa-mathlib yra atskiros viešos teoremų paketų repozitorijos finitefield-org organizacijoje. | Patikrintas viešas teiginys | S01 / S02 / 2026-07-02 | Jei publikavimas vėluoja arba keičiasi repozitorijos, dar kartą patikrinti matomumą. |
| CL-006 | npa, npa-std ir npa-mathlib repozitorijos viešuose LICENSE metaduomenyse nurodo Apache-2.0 licenciją. | Patikrintas viešas teiginys | S01 / S02 / 2026-07-02 | Didelio leidimo metu pakartotinai patikrinti LICENSE. |
Repozitorijos ir licencija
Aiškiai rodykite kodą, paketų repozitorijas ir organizacijos matomumą.
Repozitorijų nuorodos yra viešųjų šaltinių rodyklės, o ne garantija, kad dabartinis puslapis sinchronizuotas su naujausia GitHub būsena.
4 repozitorijos
finitefield-org
npa
Nuo sertifikato pradedama įrodymų asistavimo ir tikrinimo įrankių grandinė.
- Licencija
- Apache-2.0 patikrinta pagal LICENSE 2026-07-02.
- Patikrinimas
- Naujausia git žyma: v0.2.0. Naujausias GitHub leidimas nepaskelbtas. README dabartinė įrankių grandinės nuoroda: NPA_GIT_TAG=v0.2.0.
eksperimentinisRust / OCamlnuo sertifikato
Atverti repozitoriją
finitefield-org
npa-std
Standartinių teoremų paketų repozitorija NPA įrodymų šaltiniams.
- Licencija
- Apache-2.0 patikrinta pagal LICENSE 2026-07-02.
- Patikrinimas
- Naujausia git žyma ir GitHub leidimas: v0.1.0. README paketo metaduomenų versija: 0.1.0; paketo įrankių grandinės fiksuota reikšmė: NPA_GIT_TAG=v0.1.1.
eksperimentinisteoremų paketasįrodymo šaltinis
Atverti repozitoriją
finitefield-org
npa-mathlib
Formaliosios matematikos bibliotekos tyrimų repozitorija.
- Licencija
- Apache-2.0 patikrinta pagal LICENSE 2026-07-02.
- Patikrinimas
- Naujausia git žyma: v0.1.30. Naujausias GitHub leidimas: v0.1.9. README paketo metaduomenų versija: 0.2.1; paketo įrankių grandinės fiksuota reikšmė: NPA_GIT_TAG=v0.1.1.
tyrimasformalioji matematikabiblioteka
Atverti repozitoriją
finitefield-org
Finite Field GitHub organizacija
Vieša Lab repozitorijų šeimos organizacijos momentinė kopija.
- Licencija
- Taikomos konkrečių repozitorijų licencijos
- Patikrinimas
- npa, npa-std ir npa-mathlib yra viešos pagal 2026-07-02 GitHub API patikrą.
viešas indeksasmatomumo momentinė kopijašaltinis
Atverti organizaciją
Dabartinės paieškos neatitiko nė viena repozitorija.
GitHub repozitorijos yra viešo kodo būsenos šaltinis. Licencija, dabartinės žymos, viešas matomumas ir leidimų formuluotės kaip M10-T14 galutinis patikrinimas patikrintos 2026-07-02.
Įrodymų ekosistemos apsauga
Prieš lygindami įrodymų įrankius paaiškinkite jų vaidmenis.
Tai vaidmenų lentelė, o ne reitingas. Lean ir Rocq išlieka atskaitinėmis įrodymų asistentų ekosistemomis; NPA pateikiamas kaip į sertifikatus orientuotas tyrimų ir įgyvendinimo darbas.
| Elementas | Lean | Rocq | NPA |
|---|---|---|---|
| Pozicija | Atvirojo kodo programavimo kalba ir įrodymų asistentas. | Interaktyvus teoremų įrodiklis su ilga tyrimų istorija. | Tyrimų ir įgyvendinimo repozitorija, skirta nuo sertifikato pradedamam tikrinimui. |
| Tipinis naudojimas | Matematika, programinės įrangos tikrinimas ir programavimas. | Matematika, specifikacijos, programų tikrinimas ir išgavimas. | Tyrimai apie įrodymo sertifikatus, nepriklausomą tikrinimą ir mažą patikimą bazę. |
| Įrodymų riba | Jo paties patikimas branduolys ir ekosistema apibrėžia tikrinimo ribą. | Jo paties branduolys ir patikrinti kūriniai apibrėžia tikrinimo ribą. | Kanoninis .npcert artefaktas pereina iš generavimo į tikrinimą. |
| Kaip šis puslapis tai vertina | Mokymosi, palyginimo ir sąveikumo atskaita. | Mokymosi, palyginimo ir formalizavimo metodų atskaita. | Finite Field tyrimų projektas, o ne produkto pažadas. |
| Riba | Vis dar reikia specialisto žinių. | Vis dar reikia specialisto žinių. | Šiuo metu NPA nėra praktinis Lean ar Rocq pakaitalas. |
Šaltiniai
Šaltinių žemėlapį publikuokite šalia interpretacijos.
Šaltiniai rodomi tam, kad skaitytojas matytų, kurie teiginiai kyla iš viešų repozitorijų, oficialių įrodymų įrankių svetainių ir įmonės konteksto.
S01
finitefield-org/npa
Pirminis šaltinis NPA paskirčiai, pasitikėjimo modeliui, v0.2.0 dabartinės repozitorijos žymos formuluotei, komandoms, repozitorijos struktūrai ir licencijai.
Atverti šaltinį S02Finite Field GitHub organizacija
Pirminis šaltinis viešam repozitorijų matomumui, naujausioms git žymoms, leidimų puslapiams ir Lab repozitorijų šeimos momentinei kopijai, patikrintai 2026-07-02.
Atverti šaltinį S03Oficiali Lean svetainė
Pirminis šaltinis viešam Lean pozicionavimui, patikrintas 2026-07-02.
Atverti šaltinį S04Lean kalbos dokumentacija
Pirminis šaltinis priklausomų tipų teorijos ir branduolio atskaitos kontekstui, patikrintas 2026-07-02.
Atverti šaltinį S05Oficiali Rocq Prover svetainė
Pirminis šaltinis viešam Rocq pozicionavimui, patikrintas 2026-07-02.
Atverti šaltinį S06FINITE FIELD įmonės svetainė
Įmonės šaltinis Finite Field prekės ženklui ir verslo kontekstui.
Atverti šaltinįDUK
NPA būsena ir tikrinimo ribos.
Atsakymai pabrėžia pasitikėjimo ribą prieš skaitytojams supainiojant tyrimų puslapį su įdiegta įrodymų asistento paslauga.
Skaityti apie įmonę01 Ar šis puslapis yra produkto garantija?
Ne. NPA čia rodomas kaip tyrimų ir įgyvendinimo repozitorija. Klientų projektams vis tiek reikia atskirų reikalavimų, rizikos, atsakomybės ir priėmimo kriterijų.
02 Ar NPA gali pakeisti Lean arba Rocq?
Ne. NPA nėra praktinis Lean ar Rocq pakaitalas. Puslapis šią ribą palieka matomą, nes ji svarbi lūkesčiams.
03 Ar puslapis vykdo tikrą NPA patikrą?
Ne. Naršyklės simuliacija nevykdo paties NPA, Rust, WASM ar tikrų įrodymo sertifikatų. Ji paaiškina tikrinimo tvarką.
04 Kas čia laikoma įrodymu?
Tikrinimo pusės įrodymus sudaro sertifikato artefaktas, deterministinės maišos, Rust branduolio / tikrintuvo rezultatas, be šaltinio veikiantis etaloninio tikrintuvo rezultatas ir aksiomų ataskaita.
05 Kuriuos faktus reikia tikrinti pakartotinai?
Dabartinė vieša versija, repozitorijų matomumas, įrankių grandinės fiksuotos versijos, licencijos tekstas ir šaltinių formuluotės pakartotinai patikrintos 2026-07-02; jei publikavimas vėluoja arba repozitorijos keičiasi, jas reikia tikrinti dar kartą.
Nuo įrodymų disciplinos prie operacijų
Tą pačią įrodymų discipliną taikykite tada, kai verslo sprendimu reikia pasitikėti.
Verslo sistemoms naudinga pamoka nėra visur pridėti teoremų įrodymą. Svarbu nuspręsti, kas turi būti generuojama, tikrinama, registruojama, taisoma ir tvirtinama žmonių.