公開状態
研究・実装リポジトリ
GitHub リポジトリは公開されていますが、このページは運用中のサービスではなく、研究・実装リポジトリとして説明します。
Math Lab に戻る
NPA / Certificate-first proof checking
NPA: 結果を信頼する前に、証明の証拠境界を見える化する。
Math Lab の NPA セクションを独立した evidence page として再構成します。公開状態、trust model、proof pipeline、claim register、repositories、sources、Lean / Rocq の代替ではない説明をまとめます。
- 公開状態
- 研究・実装リポジトリ
- 本番保証サービスではなく、研究・実装として示します。
- 公開情報再確認
- 2026-07-02 / NPA v0.2.0
- 最新 git tag: npa v0.2.0、npa-std v0.1.0、npa-mathlib v0.1.30。
- ライセンス
- Apache-2.0
- 2026-07-02 に npa、npa-std、npa-mathlib で Apache-2.0 を確認済み。
公開情報再確認: 2026-07-02。NPA リポジトリの最新 git tag は v0.2.0、npa-std は v0.1.0、npa-mathlib は v0.1.30 です。パッケージ README の pin はリポジトリ固有の文脈として表示し、NPA 全体の単一バージョン主張にはまとめません。
Public status
公開されているもの、証拠となるもの、確認した日付を示す。
このページの根拠を見える化します。ローカル truth snapshot、公開リポジトリ source、公開前の最終確認日を分けて示します。
公開情報再確認
2026-07-02
公開情報の readback は 2026-07-02 に完了しました。元の素材再構成は引き続き 2026-06-21 のローカル truth snapshot を基準にします。
Evidence
Certificates and hashes
元スナップショットは canonical .npcert、certificate_hash、export_hash、axiom_report_hash、checker verdict を記録しています。
License
Apache-2.0 確認済み
2026-07-02 に、npa、npa-std、npa-mathlib の公開 LICENSE metadata で Apache-2.0 を確認済みです。
Boundary
NPA は Lean や Rocq の実用代替ではありません。配布版の検査シミュレーションは NPA 本体を実行しません。public tag、license、repository visibility は最終公開 readback として 2026-07-02 に確認済みです。
Trust boundary
canonical certificate だけを evidence boundary の向こう側へ渡す。
境界の論点は、どの tool が高度に見えるかではありません。independent checking 後に、どの artifact を証拠として扱えるかです。
Parser、elaborator、tactics、automation、theorem search、plugins、AI systems、source files、replay files、theorem indexes、publish plans、CI status、release pages、registry metadata は untrusted candidate side に残します。
Proof pipeline / 説明用シミュレーション
certificate bytes から checking evidence までの pipeline を示す。
配布版の検査シミュレーションは NPA 本体、Rust、WASM、実際の proof certificate を実行しません。実際の artifact が満たすべき source-free checking の順序を可視化します。
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
説明用 pipeline はまだ実行されていません。説明を実行すると、source-free checking path を順番に表示します。
Claim register
証拠、時間依存の事実、境界主張を分ける。
このページは曖昧な研究紹介に依存しません。公開する各主張を、ローカル truth snapshot、出典、公開前の対応に結び付けます。
| 主張 | 公開文言 | 状態 | 出典 | 公開前の対応 |
|---|---|---|---|---|
| CL-001 | NPA は certificate-first です。監査できる境界は canonical .npcert と、その周辺の検査経路です。 | 確認済みの公開主張 | S01 / 2026-07-02 | README 変更時に見直す。 |
| CL-002 | 2026-07-02 の公開情報再確認では、NPA リポジトリの最新 git tag は v0.2.0 でした。関連パッケージの README にはリポジトリごとの pin が残るため、版の表記はリポジトリ単位に限定します。 | 公開情報再確認済み | S01 / S02 / 2026-07-02 | tag 表記はリポジトリ単位に限定する。 |
| CL-003 | ローカル truth snapshot は Rust 1.95.0 の toolchain pin を記録しています。宣伝上の主張としては使いません。 | 確認済み・時間依存 | S01 / 2026-07-02 | toolchain 版を表示する場合だけ再確認する。 |
| CL-004 | NPA は Lean や Rocq の実用代替ではありません。比較の横にこの境界を必ず残します。 | 確認済みの境界主張 | S01 / S03 / S05 / 2026-07-02 | 注意書きを維持する。 |
| CL-005 | npa-std と npa-mathlib は、finitefield-org 上で公開されている独立した theorem package リポジトリです。 | 確認済みの公開主張 | S01 / S02 / 2026-07-02 | 公開が遅れた場合やリポジトリ変更時に再確認する。 |
| CL-006 | npa、npa-std、npa-mathlib の各公開リポジトリは、LICENSE metadata で Apache-2.0 を示しています。 | 確認済みの公開主張 | S01 / S02 / 2026-07-02 | 主要リリース時に LICENSE を再確認する。 |
Repositories and license
コード、package repository、organization visibility を明示する。
Repository link は公開 source への参照であり、このページが最新の GitHub 状態と常に同期している保証ではありません。
4 件を表示
finitefield-org
npa
certificate-first な proof assistance と verification の toolchain。
- License
- 2026-07-02 に LICENSE で Apache-2.0 を確認済み。
- Verification
- 最新 git tag: v0.2.0。GitHub releases/latest は未公開。README の現行 toolchain reference: NPA_GIT_TAG=v0.2.0。
experimentalRust / OCamlcertificate-first
リポジトリを開く
finitefield-org
npa-std
NPA proof source の standard theorem package repository。
- License
- 2026-07-02 に LICENSE で Apache-2.0 を確認済み。
- Verification
- 最新 git tag と GitHub release: v0.1.0。README の package metadata version: 0.1.0、package toolchain pin: NPA_GIT_TAG=v0.1.1。
experimentaltheorem packageproof source
リポジトリを開く
finitefield-org
npa-mathlib
formal mathematics library の研究リポジトリ。
- License
- 2026-07-02 に LICENSE で Apache-2.0 を確認済み。
- Verification
- 最新 git tag: v0.1.30。最新 GitHub release: v0.1.9。README の package metadata version: 0.2.1、package toolchain pin: NPA_GIT_TAG=v0.1.1。
researchformal mathematicslibrary
リポジトリを開く
finitefield-org
Finite Field GitHub organization
Lab repository family の公開組織スナップショット。
- License
- repository ごとの license が適用されます
- Verification
- 2026-07-02 の GitHub API readback で npa、npa-std、npa-mathlib は公開リポジトリ。
public indexvisibility snapshotsource
組織を開く
現在の検索条件に一致するリポジトリはありません。
GitHub リポジトリが公開コード状態の source です。license、current tags、public visibility、release wording は M10-T14 の最終 readback として 2026-07-02 に確認済みです。
Proof ecosystem guard
Proof tool を比較する前に、役割を明確にする。
これは順位表ではなく役割表です。Lean と Rocq は参照すべき proof assistant ecosystem であり、NPA は certificate-centered な研究・実装として示します。
| 項目 | Lean | Rocq | NPA |
|---|---|---|---|
| 位置づけ | オープンソースの programming language 兼 proof assistant。 | 長い研究史を持つ interactive theorem prover。 | certificate-first な検査のための研究・実装リポジトリ。 |
| 主な用途 | 数学、ソフトウェア検証、プログラミング。 | 数学、仕様、プログラム検証、抽出。 | proof certificate、独立検査、小さな trusted base の研究。 |
| 証拠境界 | Lean 自身の trusted kernel と ecosystem が検査境界を定めます。 | Rocq 自身の kernel と確認済み development が検査境界を定めます。 | canonical .npcert が generation から checking へ渡る境界になります。 |
| このページでの扱い | 学習、比較、相互運用の参照先。 | 学習、比較、formalization 手法の参照先。 | Finite Field の研究プロジェクトであり、製品保証ではありません。 |
| 境界 | 専門知識は引き続き必要です。 | 専門知識は引き続き必要です。 | 現時点で、NPA は Lean や Rocq の実用代替ではありません。 |
Sources
解釈の横に source map を公開する。
公開リポジトリ、proof tool 公式サイト、会社文脈のどこに由来する主張かを読者が確認できるよう、source map を併記します。
S01
finitefield-org/npa
NPA の purpose、trust model、現行リポジトリ tag v0.2.0、commands、repository layout、license の primary source。
出典を開く S02Finite Field GitHub organization
2026-07-02 に確認した public repository visibility、latest git tags、release pages、Lab repository family snapshot の primary source。
出典を開く S03Lean official site
Lean の公開上の位置づけに関する primary source。2026-07-02 確認。
出典を開く S04Lean language reference
dependent type theory と kernel reference context の primary source。2026-07-02 確認。
出典を開く S05Rocq Prover official site
Rocq の公開上の位置づけに関する primary source。2026-07-02 確認。
出典を開く S06FINITE FIELD company site
Finite Field の brand と business context の company source。
出典を開く01 このページは製品保証ですか。
いいえ。NPA は研究・実装リポジトリとして示しています。
02 NPA は Lean や Rocq を置き換えられますか。
いいえ。NPA は Lean や Rocq の実用代替ではありません。
03 このページは本物の NPA verification を実行しますか。
いいえ。配布版の検査シミュレーションは NPA 本体、Rust、WASM、実際の proof certificate を実行しません。
04 ここで証拠とみなすものは何ですか。
certificate artifact、deterministic hash、Rust kernel/verifier result、source-free reference checker result、axiom report が checking side の証拠になります。
05 どの事実を再確認しますか。
公開中の版、リポジトリ公開状態、toolchain pin、ライセンス文言、出典文言は 2026-07-02 に再確認済みです。