代数、解析、位相
catalog には groups、rings、metric spaces、topology、vector modules と関連する theorem clusters が含まれます。
NPAに戻る
NPA package
npa-mathlib: Nano Proof Auditor のための形式化数学。
このパッケージは、NPA site が使う public theorem-library corpus を収めています。ページは /npa/mathlib/ に置き、今後の theorem introductions を同じブランド所有URL配下で増やせるようにします。
Package role
今後の定理紹介を増やせる数学ライブラリページ。
移植元の npa-site package page は exported modules と auditing commands を表示します。このサイト版ではその構造を残しつつ、URLを NPA strategy document に合わせます。
Certificate-backed modules
代表的な mathlib modules は、source catalog で verified_by_certificate として示されています。
短いURL
NPA という文脈が package family を示すため、/npa/npa-mathlib/ ではなく /npa/mathlib/ を使います。
定理紹介に拡張しやすい構造
ライブラリ紹介から個別 theorem introductions へリンクできるよう、パッケージ概要を安定URLに置きます。
Exported modules
source catalog から抜粋した代表モジュール。
この一覧は npa-site からの selected readback であり、full theorem browser ではありません。生成済みカタログ全体を移植せず、package scope を見える状態にします。
Module
Theorems
Imports
Status
Mathlib.Algebra.Group.Basic
/pkg/Mathlib/Algebra/Group/Basic/
Theorems: 23
Imports: 2
verified_by_certificate
Mathlib.Algebra.Group.Correspondence
/pkg/Mathlib/Algebra/Group/Correspondence/
Theorems: 8
Imports: 8
verified_by_certificate
Mathlib.Algebra.Group.Correspondence.Basic
/pkg/Mathlib/Algebra/Group/Correspondence/Basic/
Theorems: 18
Imports: 7
verified_by_certificate
Mathlib.Algebra.Group.FirstIsomorphism
/pkg/Mathlib/Algebra/Group/FirstIsomorphism/
Theorems: 5
Imports: 8
verified_by_certificate
Mathlib.Topology.Metric.Basic
/pkg/Mathlib/Topology/Metric/Basic/
Theorems: 15
Imports: 2
verified_by_certificate
Mathlib.Vector.Dot
/pkg/Mathlib/Vector/Dot/
Theorems: 17
Imports: 5
verified_by_certificate
Auditing
NPA commands で package を監査します。
これらは npa-site が示していた package workflow を、npa-mathlib checkout 向けに残したものです。
Certificates を監査
npa package verify-certs --root ../npa-mathlib --checker reference --jsonPolicy を検査
npa package check --root ../npa-mathlib --json