公開狀態
繁體中文：Research and implementation repository
繁體中文：The GitHub repository is public, but this page describes a research and implementation repository, not a deployed service.
Finite Field
30 秒診斷
此頁面尚未提供此語言版本。
繁體中文：Back to Math Lab
NPA / Certificate-first proof checking
繁體中文：NPA: expose the proof evidence boundary before trusting a result.
繁體中文：This page reconstructs the NPA section from Math Lab as an independent evidence page: public status, trust model, proof pipeline, claim register, repositories, sources, and explicit non-replacement language.
- 公開狀態
- 研究 repository
- 繁體中文：Shown as research and implementation, not as a production assurance service.
- 公開複核
- 2026-07-02 / NPA v0.2.0
- 繁體中文：Latest git tags checked: npa v0.2.0, npa-std v0.1.0, npa-mathlib v0.1.30.
- 授權
- Apache-2.0
- 繁體中文：Apache-2.0 was verified for npa, npa-std, and npa-mathlib on 2026-07-02.
繁體中文：Public recheck: 2026-07-02. The NPA repository latest git tag is v0.2.0; npa-std is v0.1.0; npa-mathlib is v0.1.30. Package README pins are shown as repository-specific context and are not flattened into one NPA version claim.
Public status
繁體中文：State what is public, what is evidence, and when it was rechecked.
繁體中文：This page makes the page's basis visible: a local truth snapshot, a public repository source, and the final prelaunch readback date.
Public recheck
2026-07-02
繁體中文：The public-source readback was completed on 2026-07-02. The original source reconstruction still uses the 2026-06-21 local truth snapshot.
Evidence
Certificates and hashes
繁體中文：The source snapshot records canonical .npcert, certificate_hash, export_hash, axiom_report_hash, and checker verdicts.
License
Apache-2.0 verified
繁體中文：Apache-2.0 was verified for npa, npa-std, and npa-mathlib through public LICENSE metadata on 2026-07-02.
Boundary
繁體中文：NPA is not a practical replacement for Lean or Rocq. The distributed browser inspection simulation does not run NPA itself. Public tags, license, and repository visibility were checked on 2026-07-02 for the final publication readback.
Trust boundary
繁體中文：Move only a canonical certificate across the evidence boundary.
繁體中文：The boundary is not about which tool looks sophisticated. It is about which artifact is allowed to become evidence after independent checking.
繁體中文：Parser, elaborator, tactics, automation, theorem search, plugins, AI systems, source files, replay files, theorem indexes, publish plans, CI status, release pages, and registry metadata stay on the untrusted candidate side.
繁體中文：Proof pipeline / explanatory simulation
繁體中文：Show the exact pipeline from certificate bytes to checking evidence.
繁體中文：The browser simulation does not run NPA itself, Rust, WASM, or real proof certificates. It visualizes the source-free checking order that real artifacts must satisfy.
CLI evidence path
npa package verify-certs --root . --checker reference --json
NPA / audit trace
READY
- 01 Certificate formatcanonical .npcert bytes / parseable certificate / format check WAIT
- 02 Certificate hashcertificate bytes / certificate_hash / deterministic digest WAIT
- 03 Kernel verdictcertificate / accept or reject / Rust verifier report WAIT
- 04 Reference checkerhash-pinned certificate / independent accept or reject / source-free checker report WAIT
- 05 Axiom reportchecked package / axiom_report_hash / assumption inventory WAIT
Verdict
繁體中文：The explanatory pipeline has not run yet.繁體中文：Run the explanation to mark the source-free checking path in order.
Claim register
繁體中文：Separate evidence, time-sensitive facts, and boundary claims.
繁體中文：The page does not depend on loose research copy. Each public statement is tied to a local truth snapshot, a source, and a publication action.
| 繁體中文：Claim | 繁體中文：Public wording | 狀態 | 繁體中文：Source | 繁體中文：Publication action |
|---|---|---|---|---|
| CL-001 | 繁體中文：NPA is certificate-first: the auditable boundary is the canonical .npcert artifact and the checking path around it. | 繁體中文：Verified public claim | S01 / 2026-07-02 | 繁體中文：Review when the README changes. |
| CL-002 | 繁體中文：The 2026-07-02 public recheck found the NPA repository latest git tag at v0.2.0. Related package READMEs still show repository-specific pins, so version wording stays scoped by repository. | 繁體中文：Verified public recheck | S01 / S02 / 2026-07-02 | 繁體中文：Keep tag wording scoped by repository. |
| CL-003 | 繁體中文：The local truth snapshot records a Rust 1.95.0 toolchain pin; it is not used as a marketing claim. | 繁體中文：Verified, time-sensitive | S01 / 2026-07-02 | 繁體中文：Recheck if the toolchain version is displayed. |
| CL-004 | 繁體中文：NPA is not a practical replacement for Lean or Rocq. This boundary must stay visible beside any comparison. | 繁體中文：Verified boundary claim | S01 / S03 / S05 / 2026-07-02 | 繁體中文：Retain the disclaimer. |
| CL-005 | 繁體中文：npa-std and npa-mathlib are separate public theorem-package repositories in the finitefield-org organization. | 繁體中文：Verified public claim | S01 / S02 / 2026-07-02 | 繁體中文：Recheck repository visibility again if publication is delayed or repositories change. |
| CL-006 | 繁體中文：The npa, npa-std, and npa-mathlib repositories each expose Apache-2.0 licensing through their public LICENSE metadata. | 繁體中文：Verified public claim | S01 / S02 / 2026-07-02 | 繁體中文：Recheck LICENSE on a major release. |
Repositories and license
繁體中文：Keep code, package repositories, and organization visibility explicit.
繁體中文：Repository links are public-source pointers, not guarantees that the current page is synchronized with the latest GitHub state.
4 繁體中文：repositories shown
finitefield-org
npa
繁體中文：Certificate-first proof assistance and verification toolchain.
- License
- 繁體中文：Apache-2.0 verified from LICENSE on 2026-07-02.
- Verification
- Latest git tag: v0.2.0. No latest GitHub release is published. README current toolchain reference: NPA_GIT_TAG=v0.2.0.
experimentalRust / OCamlcertificate-first
繁體中文：Open repository
finitefield-org
npa-std
繁體中文：Standard theorem package repository for NPA proof sources.
- License
- 繁體中文：Apache-2.0 verified from LICENSE on 2026-07-02.
- Verification
- 繁體中文：Latest git tag and GitHub release: v0.1.0. README package metadata version: 0.1.0; package toolchain pin: NPA_GIT_TAG=v0.1.1.
experimentaltheorem packageproof source
繁體中文：Open repository
finitefield-org
npa-mathlib
繁體中文：Formal mathematics library research repository.
- License
- 繁體中文：Apache-2.0 verified from LICENSE on 2026-07-02.
- Verification
- 繁體中文：Latest git tag: v0.1.30. Latest GitHub release: v0.1.9. README package metadata version: 0.2.1; package toolchain pin: NPA_GIT_TAG=v0.1.1.
researchformal mathematicslibrary
繁體中文：Open repository
finitefield-org
Finite Field GitHub organization
繁體中文：Public organization snapshot for the Lab repository family.
- License
- 繁體中文：Repository-specific licenses apply
- Verification
- 繁體中文：npa, npa-std, and npa-mathlib are public as of the 2026-07-02 GitHub API readback.
public indexvisibility snapshotsource
繁體中文：Open organization
繁體中文：No repository matched the current search.
繁體中文：The GitHub repositories are the source for public code status. License, current tags, public visibility, and release wording were checked on 2026-07-02 as the M10-T14 final readback.
Proof ecosystem guard
繁體中文：Clarify roles before comparing proof tools.
繁體中文：This is a role table, not a ranking. Lean and Rocq remain the reference proof-assistant ecosystems; NPA is presented as certificate-centered research and implementation work.
| 繁體中文：Item | Lean | Rocq | NPA |
|---|---|---|---|
| 繁體中文：Position | 繁體中文：Open-source programming language and proof assistant. | 繁體中文：Interactive theorem prover with a long research history. | 繁體中文：Research and implementation repository for certificate-first checking. |
| 繁體中文：Typical use | 繁體中文：Mathematics, software verification, and programming. | 繁體中文：Mathematics, specifications, program verification, and extraction. | 繁體中文：Research into proof certificates, independent checking, and a small trusted base. |
| 繁體中文：Evidence boundary | 繁體中文：Its own trusted kernel and ecosystem define the checking boundary. | 繁體中文：Its own kernel and checked developments define the checking boundary. | 繁體中文：The canonical .npcert artifact crosses from generation into checking. |
| 繁體中文：How this page treats it | 繁體中文：Reference for learning, comparison, and interoperability. | 繁體中文：Reference for learning, comparison, and formalization methods. | 繁體中文：Finite Field research project, not a product promise. |
| 繁體中文：Boundary | 繁體中文：Specialist knowledge is still required. | 繁體中文：Specialist knowledge is still required. | 繁體中文：NPA is not a practical replacement for Lean or Rocq at this time. |
Sources
繁體中文：Publish the source map beside the interpretation.
繁體中文：Sources are shown so the reader can tell which claims come from public repositories, official proof-tool sites, and company context.
S01
finitefield-org/npa
繁體中文：Primary source for NPA purpose, trust model, v0.2.0 current repository tag wording, commands, repository layout, and license.
繁體中文：Open source S02Finite Field GitHub organization
繁體中文：Primary source for public repository visibility, latest git tags, release pages, and the Lab repository family snapshot checked on 2026-07-02.
繁體中文：Open source S03Lean official site
繁體中文：Primary source for Lean's public positioning, checked on 2026-07-02.
繁體中文：Open source S04Lean language reference
繁體中文：Primary source for dependent type theory and kernel reference context, checked on 2026-07-02.
繁體中文：Open source S05Rocq Prover official site
繁體中文：Primary source for Rocq's public positioning, checked on 2026-07-02.
繁體中文：Open source S06FINITE FIELD company site
繁體中文：Company source for Finite Field brand and business context.
繁體中文：Open sourceFAQ
繁體中文：NPA status and verification boundaries.
繁體中文：The answers emphasize the trust boundary before readers confuse a research page with a deployed proof-assistant service.
繁體中文：Read about the company01 繁體中文：Is this page a product guarantee?
繁體中文：No. NPA is shown here as a research and implementation repository.
02 繁體中文：Can NPA replace Lean or Rocq?
繁體中文：No. NPA is not a practical replacement for Lean or Rocq.
03 繁體中文：Does the page run real NPA verification?
繁體中文：No. The browser simulation does not run NPA itself, Rust, WASM, or real proof certificates.
04 繁體中文：What counts as evidence here?
繁體中文：The certificate artifact, deterministic hashes, Rust kernel/verifier result, source-free reference checker result, and axiom report form the checking-side evidence.
05 繁體中文：Which facts need rechecking?
繁體中文：Current public version, repository visibility, toolchain pins, license text, and source wording were rechecked on 2026-07-02.
繁體中文：From proof discipline to operations
繁體中文：Use the same evidence discipline when a business decision must be trusted.
繁體中文：For business systems, the useful lesson is not to add theorem proving everywhere. It is to decide what must be generated, checked, logged, corrected, and approved by people.