代数、分析、拓扑
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/mathlib/，而不是 /npa/npa-mathlib/。
便于扩展定理介绍
随着库增长，单个 theorem introductions 可回链到这个稳定的 package overview。
Exported modules
从 source catalog 选取的代表模块。
该列表是从 npa-site 读取的 selected readback，不是完整 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 审计该包。
这些命令保留 npa-site 展示的 package workflow，并限定在 npa-mathlib checkout。
审计 certificates
npa package verify-certs --root ../npa-mathlib --checker reference --json检查 policy
npa package check --root ../npa-mathlib --json