Publiskais statuss
Pētījumu un ieviešanas repozitorijs
GitHub repozitorijs ir publisks, bet šī lapa apraksta pētījumu un ieviešanas repozitoriju, nevis izvietotu pakalpojumu.
Atpakaļ uz Math Lab
NPA / pierādījumu pārbaude ar sertifikātiem pirmajā vietā
NPA: pirms uzticēšanās rezultātam parādīt pierādījumu robežu.
Šī lapa pārveido Math Lab NPA sadaļu par neatkarīgu pierādījumu lapu: publisko statusu, uzticības modeli, pierādījumu plūsmu, apgalvojumu reģistru, repozitorijus, avotus un skaidru valodu, ka NPA nav aizstājējs.
- Publiskais statuss
- Pētījumu repozitorijs
- Rādīts kā pētījums un ieviešana, nevis kā ražošanas garantijas pakalpojums.
- Publiskā atkārtotā pārbaude
- 2026-07-02 / NPA v0.2.0
- Pārbaudīti jaunākie git tagi: npa v0.2.0, npa-std v0.1.0, npa-mathlib v0.1.30.
- Licence
- Apache-2.0
- Apache-2.0 tika pārbaudīta npa, npa-std un npa-mathlib repozitorijiem 2026-07-02.
Publiskā atkārtotā pārbaude: 2026-07-02. NPA repozitorija jaunākais git tags ir v0.2.0; npa-std ir v0.1.0; npa-mathlib ir v0.1.30. Pakotņu README piesaistes tiek rādītas kā konkrētu repozitoriju konteksts, nevis saplacinātas vienā NPA versijas apgalvojumā.
Publiskais statuss
Norādīt, kas ir publisks, kas ir pierādījums un kad tas tika pārbaudīts vēlreiz.
Šī lapa padara redzamu savu pamatu: lokālu patiesības momentuzņēmumu, publisku repozitorija avotu un galīgās pārbaudes datumu pirms publicēšanas.
Publiskā atkārtotā pārbaude
2026-07-02
Publiskā avota pārlase tika pabeigta 2026-07-02. Sākotnējā avota rekonstrukcija joprojām izmanto 2026-06-21 lokālo patiesības momentuzņēmumu.
Pierādījumi
Sertifikāti un jaucējvērtības
Avota momentuzņēmumā ir kanoniskais .npcert, certificate_hash, export_hash, axiom_report_hash un pārbaudītāju spriedumi.
Licence
Apache-2.0 pārbaudīta
Apache-2.0 tika pārbaudīta npa, npa-std un npa-mathlib repozitorijiem pēc publiskajiem LICENSE metadatiem 2026-07-02.
Robeža
NPA nav praktisks Lean vai Rocq aizstājējs. Pārlūkā izplatītā pārbaudes simulācija neizpilda pašu NPA. Publiskie tagi, licence un repozitoriju redzamība tika pārbaudīti 2026-07-02 gala publicēšanas pārlasei.
Uzticamības robeža
Pāri pierādījumu robežai drīkst pāriet tikai kanoniskais sertifikāts.
Robeža nav par to, kurš rīks izskatās sarežģīts. Tā ir par to, kuram artefaktam pēc neatkarīgas pārbaudes drīkst kļūt par pierādījumu.
Parseris, elaborators, taktikas, automatizācija, teorēmu meklēšana, spraudņi, AI sistēmas, avota faili, replay faili, teorēmu indeksi, publicēšanas plāni, CI statuss, laidienu lapas un reģistra metadati paliek neuzticamajā kandidātu pusē.
Pierādījumu plūsma / skaidrojoša simulācija
Parādīt precīzu plūsmu no sertifikāta baitiem līdz pārbaudes pierādījumiem.
Pārlūka simulācija neizpilda pašu NPA, Rust, WASM vai īstus pierādījumu sertifikātus. Tā vizualizē no avota neatkarīgu pārbaudes secību, kas jāizpilda īstiem artefaktiem.
CLI pierādījumu ceļš
npa package verify-certs --root . --checker reference --json
NPA / audita pēda
GATAVS
- 01 Sertifikāta formātskanoniskie .npcert baiti / parsējams sertifikāts / formāta pārbaude GAIDA
- 02 Sertifikāta jaucējvērtībasertifikāta baiti / certificate_hash / deterministisks digest GAIDA
- 03 Kodola spriedumssertifikāts / pieņemt vai noraidīt / Rust pārbaudītāja pārskats GAIDA
- 04 Atsauces pārbaudītājsar jaucējvērtību piesaistīts sertifikāts / neatkarīgi pieņemt vai noraidīt / no avota neatkarīga pārbaudītāja pārskats GAIDA
- 05 Aksiomu pārskatspārbaudīta pakete / axiom_report_hash / pieņēmumu inventārs GAIDA
Spriedums
Skaidrojošā plūsma vēl nav palaista.Palaidiet skaidrojumu, lai secīgi iezīmētu no avota neatkarīgo pārbaudes ceļu.
Apgalvojumu reģistrs
Nošķirt pierādījumus, laika ziņā jutīgus faktus un robežu apgalvojumus.
Lapa nepaļaujas uz vaļīgu pētījumu tekstu. Katrs publiskais apgalvojums ir sasaistīts ar lokālu patiesības momentuzņēmumu, avotu un publicēšanas darbību.
| Apgalvojums | Publiskais formulējums | Statuss | Avots | Publicēšanas darbība |
|---|---|---|---|---|
| CL-001 | NPA sākas ar sertifikātu: auditējamā robeža ir kanoniskais .npcert artefakts un pārbaudes ceļš ap to. | Pārbaudīts publisks apgalvojums | S01 / 2026-07-02 | Pārskatīt, kad mainās README. |
| CL-002 | 2026-07-02 publiskā atkārtotā pārbaude atrada NPA repozitorija jaunāko git tagu v0.2.0. Saistīto pakotņu README joprojām rāda konkrētiem repozitorijiem piesaistītas versijas, tāpēc versijas formulējums paliek repozitorija tvērumā. | Pārbaudīta publiska atkārtotā pārbaude | S01 / S02 / 2026-07-02 | Tagu formulējumu turēt repozitorija tvērumā. |
| CL-003 | Lokālais patiesības momentuzņēmums fiksē Rust 1.95.0 rīku ķēdes piesaisti; tā netiek izmantota kā mārketinga apgalvojums. | Pārbaudīts, laika ziņā jutīgs | S01 / 2026-07-02 | Pārbaudīt vēlreiz, ja tiek rādīta rīku ķēdes versija. |
| CL-004 | NPA nav praktisks Lean vai Rocq aizstājējs. Šai robežai jāpaliek redzamai pie jebkura salīdzinājuma. | Pārbaudīts robežas apgalvojums | S01 / S03 / S05 / 2026-07-02 | Saglabāt atrunu. |
| CL-005 | npa-std un npa-mathlib ir atsevišķi publiski teorēmu pakotņu repozitoriji finitefield-org organizācijā. | Pārbaudīts publisks apgalvojums | S01 / S02 / 2026-07-02 | Ja publicēšana kavējas vai repozitoriji mainās, vēlreiz pārbaudīt repozitoriju redzamību. |
| CL-006 | npa, npa-std un npa-mathlib repozitoriji publiskajos LICENSE metadatos katrs norāda Apache-2.0 licenci. | Pārbaudīts publisks apgalvojums | S01 / S02 / 2026-07-02 | Lielā laidienā vēlreiz pārbaudīt LICENSE. |
Repozitoriji un licence
Kodu, pakotņu repozitorijus un organizācijas redzamību turēt skaidri redzamus.
Repozitoriju saites ir publisko avotu norādes, nevis garantijas, ka pašreizējā lapa ir sinhronizēta ar jaunāko GitHub stāvokli.
4 repozitoriji parādīti
finitefield-org
npa
Pierādījumu palīdzības un verifikācijas rīku ķēde ar sertifikātiem pirmajā vietā.
- Licence
- Apache-2.0 pārbaudīta pēc LICENSE 2026-07-02.
- Pārbaude
- Jaunākais git tags: v0.2.0. Jaunākais GitHub laidiens nav publicēts. README pašreizējā rīku ķēdes norāde: NPA_GIT_TAG=v0.2.0.
eksperimentālsRust / OCamlsertifikāti pirmajā vietā
Atvērt repozitoriju
finitefield-org
npa-std
Standarta teorēmu pakotņu repozitorijs NPA pierādījumu avotiem.
- Licence
- Apache-2.0 pārbaudīta pēc LICENSE 2026-07-02.
- Pārbaude
- Jaunākais git tags un GitHub laidiens: v0.1.0. README pakotnes metadatu versija: 0.1.0; pakotnes rīku ķēdes piesaiste: NPA_GIT_TAG=v0.1.1.
eksperimentālsteorēmu paketepierādījumu avots
Atvērt repozitoriju
finitefield-org
npa-mathlib
Formālās matemātikas bibliotēkas pētījumu repozitorijs.
- Licence
- Apache-2.0 pārbaudīta pēc LICENSE 2026-07-02.
- Pārbaude
- Jaunākais git tags: v0.1.30. Jaunākais GitHub laidiens: v0.1.9. README pakotnes metadatu versija: 0.2.1; pakotnes rīku ķēdes piesaiste: NPA_GIT_TAG=v0.1.1.
pētījumsformālā matemātikabibliotēka
Atvērt repozitoriju
finitefield-org
Finite Field GitHub organizācija
Publisks organizācijas momentuzņēmums Lab repozitoriju saimei.
- Licence
- Piemēro konkrēto repozitoriju licences
- Pārbaude
- npa, npa-std un npa-mathlib ir publiski saskaņā ar 2026-07-02 GitHub API pārlasi.
publisks indekssredzamības momentuzņēmumsavots
Atvērt organizāciju
Neviens repozitorijs neatbilda pašreizējai meklēšanai.
GitHub repozitoriji ir publiskā koda statusa avots. Licence, pašreizējie tagi, publiskā redzamība un laidienu formulējums tika pārbaudīti 2026-07-02 kā M10-T14 gala pārlase.
Pierādījumu ekosistēmas aizsardzība
Pirms pierādījumu rīku salīdzināšanas noskaidrot to lomas.
Šī ir lomu tabula, nevis rangs. Lean un Rocq paliek atsauces pierādījumu palīgu ekosistēmas; NPA tiek parādīts kā sertifikātos centrēts pētījumu un ieviešanas darbs.
| Punkts | Lean | Rocq | NPA |
|---|---|---|---|
| Pozīcija | Atvērtā pirmkoda programmēšanas valoda un pierādījumu palīgs. | Interaktīvs teorēmu pierādītājs ar ilgu pētījumu vēsturi. | Pētījumu un ieviešanas repozitorijs pārbaudei ar sertifikātiem pirmajā vietā. |
| Tipisks lietojums | Matemātika, programmatūras verifikācija un programmēšana. | Matemātika, specifikācijas, programmu verifikācija un ekstrakcija. | Pētījumi par pierādījumu sertifikātiem, neatkarīgu pārbaudi un mazu uzticamo bāzi. |
| Pierādījumu robeža | Paša uzticamais kodols un ekosistēma definē pārbaudes robežu. | Paša kodols un pārbaudītās izstrādes definē pārbaudes robežu. | Kanoniskais .npcert artefakts pāriet no ģenerēšanas uz pārbaudi. |
| Kā šī lapa to traktē | Atsauce mācībām, salīdzināšanai un savietojamībai. | Atsauce mācībām, salīdzināšanai un formalizācijas metodēm. | Finite Field pētījumu projekts, nevis produkta solījums. |
| Robeža | Joprojām vajadzīgas speciālista zināšanas. | Joprojām vajadzīgas speciālista zināšanas. | Pašlaik NPA nav praktisks Lean vai Rocq aizstājējs. |
Avoti
Publicēt avotu karti blakus interpretācijai.
Avoti tiek rādīti, lai lasītājs varētu noteikt, kuri apgalvojumi nāk no publiskiem repozitorijiem, oficiālām pierādījumu rīku vietnēm un uzņēmuma konteksta.
S01
finitefield-org/npa
Primārais avots NPA mērķim, uzticības modelim, v0.2.0 pašreizējā repozitorija taga formulējumam, komandām, repozitorija struktūrai un licencei.
Atvērt avotu S02Finite Field GitHub organizācija
Primārais avots publiskajai repozitoriju redzamībai, jaunākajiem git tagiem, laidienu lapām un Lab repozitoriju saimes momentuzņēmumam, kas pārbaudīts 2026-07-02.
Atvērt avotu S03Lean oficiālā vietne
Primārais avots Lean publiskajam pozicionējumam, pārbaudīts 2026-07-02.
Atvērt avotu S04Lean valodas atsauce
Primārais avots atkarīgo tipu teorijas un kodola atsauces kontekstam, pārbaudīts 2026-07-02.
Atvērt avotu S05Rocq Prover oficiālā vietne
Primārais avots Rocq publiskajam pozicionējumam, pārbaudīts 2026-07-02.
Atvērt avotu S06FINITE FIELD uzņēmuma vietne
Uzņēmuma avots Finite Field zīmolam un biznesa kontekstam.
Atvērt avotuBUJ
NPA statuss un verifikācijas robežas.
Atbildes uzsver uzticamības robežu, pirms lasītāji sajauc pētījumu lapu ar izvietotu pierādījumu palīga pakalpojumu.
Lasīt par uzņēmumu01 Vai šī lapa ir produkta garantija?
Nē. NPA šeit tiek rādīts kā pētījumu un ieviešanas repozitorijs. Klientu projektiem joprojām vajag atsevišķas prasības, risku, atbildību un pieņemšanas kritērijus.
02 Vai NPA var aizstāt Lean vai Rocq?
Nē. NPA nav praktisks Lean vai Rocq aizstājējs. Lapa šo robežu atstāj redzamu, jo tā ietekmē gaidas.
03 Vai lapa izpilda īstu NPA verifikāciju?
Nē. Pārlūka simulācija neizpilda pašu NPA, Rust, WASM vai īstus pierādījumu sertifikātus. Tā skaidro pārbaudes secību.
04 Kas šeit skaitās pierādījums?
Sertifikāta artefakts, deterministiskas jaucējvērtības, Rust kodola vai pārbaudītāja rezultāts, no avota neatkarīga atsauces pārbaudītāja rezultāts un aksiomu pārskats veido pārbaudes puses pierādījumus.
05 Kuri fakti jāpārbauda vēlreiz?
Pašreizējā publiskā versija, repozitoriju redzamība, rīku ķēdes piesaistes, licences teksts un avotu formulējumi tika atkārtoti pārbaudīti 2026-07-02, un tie jāpārbauda vēlreiz, ja publicēšana kavējas vai repozitoriji mainās.
No pierādījumu disciplīnas uz operācijām
Izmantojiet to pašu pierādījumu disciplīnu, kad jāuzticas biznesa lēmumam.
Biznesa sistēmām noderīgā mācība nav pievienot teorēmu pierādīšanu visur. Tā ir izlemt, kas jāģenerē, jāpārbauda, jāreģistrē, jālabo un jāapstiprina cilvēkiem.