公開状態
研究・実装リポジトリ
GitHub リポジトリは公開されていますが、このページは運用中のサービスではなく、研究・実装リポジトリとして説明します。
Math Lab に戻る
NPA / 証明書を中心とした証明検査
NPA: 結果を信頼する前に、証明の信頼境界を見える化する。
このページでは、Math Lab の NPA に関する内容を一つの資料にまとめています。何が公開されているか、信頼性をどう確保するか、証明をどう検査するか、どの主張に根拠があるか、ソースリポジトリはどこにあるか、NPA が既存の証明支援系を代替しない理由を説明します。
- 公開状態
- 研究・実装リポジトリ
- 本番保証サービスではなく、研究・実装として示します。
- 公開情報再確認
- 2026-07-02 / NPA v0.2.0
- 最新 Git タグ: 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 タグは v0.2.0、npa-std は v0.1.0、npa-mathlib は v0.1.30 です。パッケージ README のバージョン固定指定はリポジトリ固有の情報として表示し、NPA 全体を単一バージョンとして扱いません。
公開状況
何が公開され、何が証拠となり、いつ最終確認したかを示す。
このページの根拠を明示します。ローカルの検証用スナップショット、公開リポジトリの情報、公開前の最終確認日を分けて示します。
公開情報再確認
2026-07-02
公開情報は 2026-07-02 に再確認しました。必要な箇所では、確認済みの 2026-06-21 時点のローカルスナップショットも参照しています。
根拠
証明書とハッシュ
元スナップショットには、正規化された .npcert、certificate_hash、export_hash、axiom_report_hash、検査器の判定が記録されています。
ライセンス
Apache-2.0 確認済み
2026-07-02 に、npa、npa-std、npa-mathlib が公開する LICENSE ファイルで Apache-2.0 を確認済みです。
適用範囲
NPA は Lean や Rocq の実用代替ではありません。このページの検査シミュレーションは NPA 本体を実行しません。公開タグ、ライセンス、リポジトリの公開状態は、最終公開前の確認として 2026-07-02 に確認済みです。
信頼境界
証拠の境界を越えられるのは、正規化された証明書だけ。
重要なのは、ツールがどれほど高度に見えるかではありません。独立検査を経た後、どの成果物を証拠として認めるかです。
構文解析器、詳細化器、証明戦略、自動化、定理検索、プラグイン、AI システム、ソースファイル、再実行用ファイル、定理索引、公開計画、CI 状態、リリースページ、登録メタデータは、信頼しない候補生成側に残します。
証明検査の流れ / 説明用シミュレーション
証明書のバイト列が、独立に検査できる証拠になるまでを正確に示す。
ブラウザ上のシミュレーションでは、NPA 本体、Rust、WebAssembly、実際の証明書を実行しません。実際の成果物が通過すべき、ソースファイルに依存しない検査順序を図示します。
CLI での検査例
npa package verify-certs --root . --checker reference --json
NPA / 監査トレース
READY
- 01 証明書形式正規化された .npcert バイト列 / 解析可能な証明書 / 形式検査 WAIT
- 02 証明書ハッシュ証明書のバイト列 / certificate_hash / 再現可能なダイジェスト WAIT
- 03 カーネルの判定証明書 / 受理または拒否 / Rust 製検査器のレポート WAIT
- 04 参照検査器ハッシュで固定された証明書 / 独立した受理または拒否 / ソース非依存の検査レポート WAIT
- 05 公理レポート検査済みパッケージ / axiom_report_hash / 前提一覧 WAIT
判定
説明用の検査手順はまだ実行されていません。説明を実行すると、ソースファイルに依存しない検査経路を順番に表示します。
主張一覧
証拠、時間とともに変わる事実、適用範囲に関する主張を分ける。
曖昧な研究紹介に頼らず、公開する各主張をローカルの事実スナップショット、出典、公開前に必要な対応へ結び付けています。
| 主張 | 公開文言 | 状態 | 出典 | 公開前の対応 |
|---|---|---|---|---|
| CL-001 | NPA は証明書を中心に設計されています。監査対象の境界は、正規化された .npcert とその周辺の検査経路です。 | 確認済みの公開主張 | S01 / 2026-07-02 | README 変更時に見直す。 |
| CL-002 | 2026-07-02 の公開情報再確認では、NPA リポジトリの最新 Git タグは v0.2.0 でした。関連パッケージの README にはリポジトリごとのバージョン固定指定があるため、版の表記はリポジトリ単位に限定します。 | 公開情報再確認済み | S01 / S02 / 2026-07-02 | Git タグの表記はリポジトリ単位に限定する。 |
| CL-003 | ローカルの検証用スナップショットには、Rust 1.95.0 のツールチェーン固定指定が記録されています。宣伝上の主張には使いません。 | 確認済み・時間依存 | S01 / 2026-07-02 | ツールチェーンのバージョンを表示する場合だけ再確認する。 |
| CL-004 | NPA は Lean や Rocq の実用代替ではありません。比較の横にこの境界を必ず残します。 | 確認済みの境界主張 | S01 / S03 / S05 / 2026-07-02 | 注意書きを維持する。 |
| CL-005 | npa-std と npa-mathlib は、finitefield-org で公開されている独立した定理パッケージのリポジトリです。 | 確認済みの公開主張 | S01 / S02 / 2026-07-02 | 公開が遅れた場合やリポジトリ変更時に再確認する。 |
| CL-006 | npa、npa-std、npa-mathlib の各公開リポジトリは、LICENSE ファイルで Apache-2.0 を示しています。 | 確認済みの公開主張 | S01 / S02 / 2026-07-02 | 主要リリース時に LICENSE を再確認する。 |
リポジトリとライセンス
コードリポジトリ、パッケージリポジトリ、公開元の組織を明示する。
リポジトリへのリンクは公開情報の参照先です。このページが GitHub の最新状態と一致することを保証するものではありません。
4 件を表示
finitefield-org
npa
証明書を中心とする証明支援・検証ツールチェーン。
- ライセンス
- 2026-07-02 に LICENSE で Apache-2.0 を確認済み。
- 確認内容
- 最新 Git タグ: v0.2.0。v0.2.0 の GitHub リリースは未公開です。README に記載された現在のツールチェーン参照値: NPA_GIT_TAG=v0.2.0。
experimentalRust / OCamlcertificate-first
リポジトリを開く
finitefield-org
npa-std
NPA の証明ソース向け標準定理パッケージのリポジトリ。
- ライセンス
- 2026-07-02 に LICENSE で Apache-2.0 を確認済み。
- 確認内容
- 最新 Git タグと GitHub リリース: v0.1.0。README のパッケージメタデータに記載されたバージョン: 0.1.0。パッケージのツールチェーン固定指定: NPA_GIT_TAG=v0.1.1。
experimentaltheorem packageproof source
リポジトリを開く
finitefield-org
npa-mathlib
形式数学ライブラリの研究リポジトリ。
- ライセンス
- 2026-07-02 に LICENSE で Apache-2.0 を確認済み。
- 確認内容
- 最新 Git タグ: v0.1.30。最新 GitHub リリース: v0.1.9。README のパッケージメタデータに記載されたバージョン: 0.2.1。パッケージのツールチェーン固定指定: NPA_GIT_TAG=v0.1.1。
researchformal mathematicslibrary
リポジトリを開く
finitefield-org
Finite Field GitHub organization
Math Lab のリポジトリ群を公開する組織のスナップショット。
- ライセンス
- 各リポジトリのライセンスが適用されます
- 確認内容
- 2026-07-02 に GitHub API で確認したところ、npa、npa-std、npa-mathlib は公開リポジトリでした。
public indexvisibility snapshotsource
組織を開く
現在の検索条件に一致するリポジトリはありません。
GitHub リポジトリを公開コードの正規情報源とします。ライセンス、現在のタグ、公開状態、リリース文言は 2026-07-02 に確認済みです。
証明支援系の比較
証明ツールを比較する前に、役割を明確にする。
これは順位表ではなく役割表です。Lean と Rocq は参照すべき証明支援系であり、NPA は証明書を中心とする研究・実装として示します。
| 項目 | Lean | Rocq | NPA |
|---|---|---|---|
| 位置づけ | オープンソースのプログラミング言語兼証明支援系。 | 長い研究史を持つ対話型定理証明器。 | 証明書を中心とする検査の研究・実装リポジトリ。 |
| 主な用途 | 数学、ソフトウェア検証、プログラミング。 | 数学、仕様、プログラム検証、抽出。 | 証明書、独立検査、小さな信頼基盤の研究。 |
| 証拠境界 | Lean 自身が信頼するカーネルと周辺環境によって、検査境界が定まります。 | Rocq 自身のカーネルと検証済みの開発成果によって、検査境界が定まります。 | 正規化された .npcert が生成側から検査側へ渡る地点が境界になります。 |
| このページでの扱い | 学習、比較、相互運用の参照先。 | 学習、比較、形式化手法の参照先。 | Finite Field の研究プロジェクトであり、製品保証ではありません。 |
| 境界 | 専門知識は引き続き必要です。 | 専門知識は引き続き必要です。 | 現時点で、NPA は Lean や Rocq の実用代替ではありません。 |
出典
解釈と、その根拠となる出典を並べて示す。
各主張が公開リポジトリ、証明ツールの公式サイト、会社情報のどこに由来するかを確認できるよう、出典対応表を併記します。
S01
finitefield-org/npa
NPA の目的、信頼モデル、現行リポジトリのタグ v0.2.0、コマンド、リポジトリ構成、ライセンスに関する一次資料。
出典を開く S02Finite Field GitHub organization
2026-07-02 に確認したリポジトリの公開状態、最新 Git タグ、リリースページ、Math Lab のリポジトリ群に関する一次資料。
出典を開く S03Lean official site
Lean の公式な位置づけに関する一次資料。2026-07-02 確認。
出典を開く S04Lean language reference
依存型理論とカーネルの参照情報に関する一次資料。2026-07-02 確認。
出典を開く S05Rocq Prover official site
Rocq の公式な位置づけに関する一次資料。2026-07-02 確認。
出典を開く S06FINITE FIELD company site
Finite Field のブランドと事業背景を説明する会社資料。
出典を開く01 このページは製品保証ですか。
いいえ。NPA は研究・実装リポジトリとして示しています。
02 NPA は Lean や Rocq を置き換えられますか。
いいえ。NPA は Lean や Rocq の実用代替ではありません。
03 このページは実際に NPA の検証を実行しますか。
いいえ。このページの検査シミュレーションは NPA 本体、Rust、WASM、実際の証明書を実行しません。
04 ここで証拠とみなすものは何ですか。
証明書ファイル、決定的ハッシュ、Rust カーネル／検証器の結果、ソースファイルに依存しない参照検査器の結果、公理レポートが、検査側の証拠になります。
05 どの事実を再確認しますか。
公開中の版、リポジトリの公開状態、ツールチェーンの固定指定、ライセンス文言、出典文言は 2026-07-02 に再確認済みです。