01 / Boundary
信頼基盤を小さく保つ
複雑な生成系や AI を信頼の中心に置かず、小さな検査側を明確にします。
Finite Field / Math Lab
速い結果だけでなく、正しさの根拠をつくる。
Math Lab は、数理モデル、定理証明、形式検証、再現性、高信頼実装を扱うときに、どこまで根拠があるかを誇張せずに示すページです。
- 公開プロジェクト
- NPA / STD / MATHLIB
- 中心言語
- Rust
- NPA スナップショット
- v0.1.1
公開情報確認日: 2026-06-28。NPA の公開状態と方法レビュー表記は確認済みです。M10-T14 で公開直前の最終 readback を行います。
Proof audit / conceptual view
閲覧専用
01 canonical bytes / format OK
02 certificate_hash OK
03 dependent proof checking OK
04 source-free verdict OK
信頼境界を見える形にする
本ページは NPA が Lean や Rocq の実用代替であるとは主張せず、ブラウザ内のシミュレーションも NPA 本体を実行しません。
Lab principle
成果だけでなく、検査の境界を公開する。
「動いた」「速かった」「証明できた」という結論だけでは足りません。入力、仮定、信頼する部分、独立して検査できる成果物、未解決事項を分けて示します。
02 / Evidence
根拠を成果物にする
証明書、ハッシュ、仮定一覧、ベンチマーク条件、ログを、他者が確認できる形で残します。
03 / Reproduce
再現性を設計する
ツールチェーン、入力データ、実行コマンド、評価基準を固定し、同じ条件で再確認できるようにします。
04 / Honesty
研究段階を誇張しない
実用方法、実験、研究を分け、限界を結果の横に置きます。
METHOD REVIEW
案件で利用可能と説明する前に、スコープ、責任範囲、案件根拠、承認を確認する方法カテゴリです。
EXPERIMENTAL
動作する実装がありますが、規模、互換性、性能、仕様変更の余地があります。バージョンと再現手順が必要です。
RESEARCH
設計、評価、証明、実装を継続中です。商用提供や完成を意味しません。
研究ポートフォリオ
研究領域を、段階と成果物で見る。
各カードには成熟度、成果物、現在の状態、次の検証を表示します。検索とフィルタはブラウザ内だけで処理します。
8件を表示
EXPERIMENTAL
OPEN SOURCE
01
Nano Proof Auditor
Certificate-first proof toolchain
依存型証明を対象に、canonical proof certificate と小さな検査基盤を中心に置く研究用ツールチェーンです。
- 成果物
- source / specification / CI templates
- 現在
- v0.1.1 public snapshot
- 次の検証
- 外部定理パッケージと独立検査
EXPERIMENTAL
OPEN SOURCE
02
NPA Standard Library
Logic / Nat / List / Algebra
NPA で再利用する基礎定理パッケージの公開リポジトリです。
- 成果物
- source / proof packages
- 現在
- public split repository
- 次の検証
- パッケージ範囲と互換性
RESEARCH
OPEN SOURCE
03
NPA Math Library
Formal mathematics library
数学定理を、独立検査できる proof package として蓄積するためのライブラリ構成です。
- 成果物
- source / proof packages
- 現在
- public repository under development
- 次の検証
- ライブラリ構造と依存関係監査
METHOD REVIEW
METHOD
04
制約付き計画モデル
Scheduling / Routing / Assignment
シフト、訪問、配車、工程、担当割り当てを、必須条件と評価指標に分ける設計方法です。
- 成果物
- model / prototype / explanation report
- 現在
- 方法レビューとして表示。導入実績は主張しません。
- 次の検証
- 案件根拠とスコープ承認
RESEARCH
MEASUREMENT
05
再現可能なソルバー評価
Benchmark and evidence
問題集合、ハードウェア、時間制限、乱数種、生ログを固定してから性能主張を行うための研究プログラムです。
- 成果物
- benchmark registry / raw logs / report
- 現在
- research-program design
- 次の検証
- 最初の公開ベンチマークコーパス
RESEARCH
FORMAL METHODS
06
重要業務ロジックの検証
Invariants for business systems
料金、権限、在庫、状態遷移などを、仕様と不変条件に分ける研究です。
- 成果物
- specification / invariants / test or proof report
- 現在
- scope study
- 次の検証
- 本番に近い限定ケースを選ぶ
EXPERIMENTAL
ENGINEERING
07
Rust による小さな信頼基盤
Small trusted components
検査器やハッシュなど、信頼の中心になる部品を小さく保つ実装方法です。
- 成果物
- NPA kernel / certificate crate / reference checker
- 現在
- public implementation in NPA
- 次の検証
- 独立検査器との互換性
RESEARCH
AI × PROOF
08
AI 支援と独立検査
Generate freely, verify strictly
AI を候補生成側に置き、最終証拠は独立検査する構成を研究します。
- 成果物
- candidate generator / certificate / checker report
- 現在
- NPA trust model と整合する研究方向
- 次の検証
- 実測した authoring workflow
一致する研究領域がありません。
別の語句で検索するか、成熟度フィルタをすべてに戻してください。
Nano Proof Auditor
証明を作る系と、信じる根拠を分ける。
NPA は依存型証明を対象にした certificate-first の証明ツールチェーンです。フロントエンド、タクティク、定理探索、プラグイン、AI、ソース、CI 表示は候補生成を助けますが、信頼済みの証明根拠ではありません。
EXPERIMENTALOPEN SOURCEAPACHE-2.0
現行スナップショット
v0.1.1
公開情報確認日: 2026-06-21。
主な中核
Rust
Rust verifier と kernel は検査側に位置づきます。
監査成果物
.npcert
Canonical certificate bytes が検査対象です。
再確認点
manual review
公開前にリポジトリ状態と package visibility を確認します。
信頼境界エクスプローラ
何を信頼し、何を信頼しないかを確認する。
各ノードを選ぶと、その役割、入力、出力、まだ必要な検査を確認できます。
UNTRUSTED
CHECKED
重要な境界
NPA は現在、Lean や Rocq の実用代替ではありません。本ページは証明書中心の研究設計を説明するもので、商用システムの無欠陥や定理の自動解決を保証しません。
証明書検査 / 説明用シミュレーション
証明書が検査される流れを体験する。
ブラウザ上の操作は、検査工程の説明です。NPA、Rust、WASM、実際の証明書は実行しません。
CLI 例
npa package verify-certs --root . --checker reference --json
NPA / audit trace
READY
- 01 証明書を読み込むcanonical bytes / format WAIT
- 02 証明書ハッシュを確認certificate_hash WAIT
- 03 カーネルで検査dependent proof checking WAIT
- 04 参照検査器で再検査source-free verdict WAIT
- 05 公理報告を照合axiom report hash WAIT
判定
まだ説明は実行されていません。実行すると、各工程を順番に可視化します。
証明系の位置づけ
優劣ではなく、役割を明確にする。
Lean と Rocq は成熟した証明支援系です。NPA は優劣比較ではなく、証明書中心の研究・実装プロジェクトとして位置づけます。
| 項目 | Lean | Rocq | NPA |
|---|---|---|---|
| 位置づけ | オープンソースのプログラミング言語・証明支援系。 | 長い研究史を持つ対話型定理証明支援系。 | certificate-first な検査を研究する実装リポジトリ。 |
| 主な用途 | 数学、ソフトウェア検証、プログラミング。 | 数学、仕様、プログラム検証、抽出。 | 証明書と独立検査の研究。 |
| 強調点 | 拡張性、ライブラリ、対話的証明。 | 表現力、成熟した方法論、ライブラリ。 | 小さな信頼基盤と canonical certificate。 |
| 本ページでの扱い | 学習、比較、相互運用の参照。 | 学習、比較、形式化技法の参照。 | Finite Field の研究プロジェクト。 |
| 境界 | 用途に応じた専門知識が必要です。 | 用途に応じた専門知識が必要です。 | 現時点で Lean や Rocq の実用代替を意図しません。 |
研究方法
「できた」を、再確認できる手順へ変える。
結果は、同じ条件で再実行でき、確認でき、反証できるときに強い根拠になります。
Question
性能、正しさ、互換性、適用範囲など、何を確かめるのかを定義します。
Assumptions
前提、除外範囲、公理、データ欠損、偏りを評価前に書き出します。
Artifact
ソース、証明書、入力、実行ログ、ハッシュを残します。
Independent check
生成側とは別の経路で結果を確認します。
Benchmark
ハードウェア、バージョン、時間制限、問題集合、乱数種を固定します。
Limits
失敗例、未対応ケース、性能限界、次の検証課題を公開します。
再現可能性ビルダー
研究公開に足りない項目を確認する。
チェックリストはブラウザ内だけで処理されます。品質認証スコアではありません。
準備度
0%次の作業
まず研究質問と成功条件を定義してください。成果物の形式より先に、何を比較・検査するかを固定します。
公開成果
公開成果を同じ入口から追跡する。
ページ表示時に GitHub API へ依存しません。リポジトリ状態はレビュー済みスナップショットで、公開前に再確認します。
4 artifacts
finitefield-org
npa
certificate-first proof toolchain
Rust / OCamlApache-2.0Experimental
開く
finitefield-org
npa-std
standard theorem package
ProofsPackageExperimental
開く
finitefield-org
npa-mathlib
formal mathematics library
MathematicsProofsResearch
開く
GitHub
finitefield-org
public repository index
OrganizationOpen source
開く
一致する公開成果がありません。
公開方針
公開リポジトリ、研究ノート、ベンチマークには、確認日、成熟度、再実行手順、既知の制約を付けます。スター数やコミット数は研究品質の指標として表示しません。
研究から業務へ
研究の作法を、業務システム設計へ持ち込む。
すべての業務システムに定理証明が必要なわけではありません。重要なのは、何を信頼し、何を比較し、何を検査し、どこを人が修正・承認するかを設計に持ち込むことです。
Lab の作法
生成、計算、最終検査を分け、すべての層を同じ強さで信頼しない設計にします。
入力、出力、証明書、ハッシュ、ログを、後から確認できる成果物として残します。
結果を比較する前に、データ、バージョン、コマンド、評価条件を固定します。
制約、失敗例、未解決事項を、成果と同じ重さで公開します。
業務システム
誰が入力し、誰が確認し、誰が修正し、誰が確定するかを定義します。
制約、評価点、除外候補、未解決事項を表示します。
条件変更、計算実行、最終承認の履歴を残します。
自動出力を現場担当者が修正、却下、説明できるようにします。
研究ノート
更新履歴と根拠を、読みやすい形で残す。
すべてのカードが公開済み記事ではありません。準備中ノートは、日付、根拠、再現手順が付くまで公開済み成果に見せません。
NPA / Current
証明書を中心に据える理由
最終的な根拠を、標準化された証明書と小さな独立検査経路に置く理由を整理します。
公開リポジトリを見るDesign note / planned
最適化結果を説明可能にする
目的、必須制約、希望条件、未割り当て理由を UI に出す設計ノートです。
関連デモを見るBenchmark / planned
ソルバー比較を公平にする条件
問題集合、時間制限、最適性ギャップ、乱数種、ハードウェア条件に関する予定ノートです。
公開基準を見る「準備中」は公開済み記事ではありません。公開後に日付、ソース、著者、再現手順、既知の制約を付与します。
01 Math Lab は受託開発サービスですか？
いいえ。研究姿勢と成果物を公開する場所です。案件相談では、適用できる方法、追加検証が必要な方法、研究段階の内容を分けて説明します。
02 NPA は Lean や Rocq の代わりに使えますか？
いいえ。現在の NPA は Lean や Rocq の実用代替ではありません。証明書、独立検査、小さな信頼基盤を中心にした研究・実装プロジェクトです。
03 AI が作った証明をそのまま信頼しますか？
そのままは扱いません。AI、探索、タクティクは候補生成を支援する側です。最終的な証明書が、それらの生成経路から独立した検査器に受理されるかを重視します。
04 形式検証を使えばバグは完全になくなりますか？
いいえ。形式手法は、明示した仕様に対して特定の性質を確認する方法です。仕様の誤り、対象外コード、運用、外部サービスは別途確認が必要です。
05 業務システムの相談にも関係しますか？
関係します。ただし通常は段階的に適用します。制約、結果理由、計算履歴、権限境界、重要業務ロジックの検査などから始めます。
Source snapshot / 2026-06-21
NPA の主張は finitefield-org/npa リポジトリのスナップショットに基づきます。Lean と Rocq の位置づけは各公式サイトに基づきます。リポジトリ状態、最新タグ、方法レビュー表記は 2026-06-28 に確認済みです。M10-T14 で公開直前の最終 readback を行います。