01 / Boundary
保持可信基小而清晰
不要把复杂生成器或 AI 放在信任中心。应明确展示较小的检查侧。
Finite Field / Math Lab
构建正确性的证据，而不只是快速结果。
Math Lab 展示我们如何处理数学建模、定理证明、形式化验证、可复现性和可信实现，同时不过度夸大证据。
- 公开项目
- NPA / STD / MATHLIB
- 核心语言
- Rust
- NPA 快照
- v0.1.1
公开信息复核: 2026-06-28。NPA 公开状态和方法复核表述已确认；M10-T14 仍需发布前最终 readback。
证明审计 / 概念视图
只读
01 canonical bytes / format OK
02 certificate_hash OK
03 dependent proof checking OK
04 source-free verdict OK
信任边界可见
本页不声称 NPA 是 Lean 或 Rocq 的实用替代品，浏览器模拟也不会执行 NPA。
Lab 原则
不仅发布结果，也发布检查边界。
“能运行”“速度快”或“已证明”这样的结论本身不够。我们会把输入、假设、可信部分、可独立检查的成果物和未解决问题分开呈现。
02 / Evidence
让证据成为成果物
把证书、哈希、假设列表、基准条件和日志留下来，方便他人检查。
03 / Reproduce
为可复现性设计
固定工具链、输入数据、执行命令和评价标准，使结果能够再次检查。
04 / Honesty
不过度表述研究状态
把实用方法、实验和研究分开呈现。限制条件应放在结果旁边。
METHOD REVIEW
这是在说明可用于项目之前，仍需确认范围、责任、项目证据和批准的方法类别。
EXPERIMENTAL
已有可运行实现，但规模、兼容性、性能或规格仍可能变化。必须附带版本和复现步骤。
RESEARCH
设计、评价、证明或实现仍在进行中。这不意味着商业可用或已经完成。
研究组合
按成熟度和成果物查看研究。
每张卡片都显示成熟度、成果物、当前状态和下一步验证。搜索与筛选只使用浏览器端状态。
8 项
EXPERIMENTAL
OPEN SOURCE
01
Nano Proof Auditor
证书优先的证明工具链
一个研究工具链，把规范化证明证书和小型检查基放在依赖证明复核的中心。
- 成果物
- source / specification / CI templates
- 当前
- v0.1.1 public snapshot
- 下一步验证
- external theorem packages and independent checking
EXPERIMENTAL
OPEN SOURCE
02
NPA Standard Library
Logic / Nat / List / Algebra
用于复用 NPA 基础内容的标准定理包仓库。
- 成果物
- source / proof packages
- 当前
- public split repository
- 下一步验证
- package scope and compatibility
RESEARCH
OPEN SOURCE
03
NPA Math Library
形式化数学库
将数学定理作为可独立检查的证明包保存的库方向。
- 成果物
- source / proof packages
- 当前
- public repository under development
- 下一步验证
- library structure and dependency audit
METHOD REVIEW
METHOD
04
约束规划模型
排程 / 路线 / 分配
在排班、拜访、路线、生产和分配工作中，分离硬约束与评价指标的方法。
- 成果物
- model / prototype / explanation report
- 当前
- 按方法复核展示，不主张部署成果。
- 下一步验证
- client evidence and scope approval
RESEARCH
MEASUREMENT
05
可复现的求解器评价
基准与证据
在提出性能主张前，先固定实例集、硬件、时间限制、随机种子和原始日志的计划。
- 成果物
- benchmark registry / raw logs / report
- 当前
- research-program design
- 下一步验证
- first public benchmark corpus
RESEARCH
FORMAL METHODS
06
关键业务逻辑验证
业务系统的不变量
研究如何把费用、权限、库存和状态迁移分离为规格与不变量。
- 成果物
- specification / invariants / test or proof report
- 当前
- scope study
- 下一步验证
- select one bounded production-like case
EXPERIMENTAL
ENGINEERING
07
Rust 中的小型可信组件
小型可信组件
把检查器和哈希等信任关键组件控制在可检查范围内的实现工作。
- 成果物
- NPA kernel / certificate crate / reference checker
- 当前
- public implementation in NPA
- 下一步验证
- independent checker compatibility
RESEARCH
AI × PROOF
08
AI 辅助与独立检查
自由生成，严格验证
一种研究方向：AI 位于候选生成侧，最终证据必须被独立检查。
- 成果物
- candidate generator / certificate / checker report
- 当前
- research direction consistent with NPA trust model
- 下一步验证
- measured authoring workflow
没有找到匹配的研究领域。
请换一个关键词，或把成熟度筛选改回全部。
Nano Proof Auditor
把证明生成和真正信任的对象分开。
NPA 是面向依赖证明的证书优先证明工具链。前端、tactic、定理搜索、插件、AI、源文件和 CI 状态都可以帮助生成候选，但它们不是可信证明证据。
EXPERIMENTALOPEN SOURCEAPACHE-2.0
当前快照
v0.1.1
公开信息于 2026-06-21 确认。
主要核心
Rust
Rust 验证器和内核属于检查侧。
审计成果物
.npcert
规范化证书字节是需要检查的对象。
复查点
manual review
发布前必须复核仓库状态和包可见性。
信任边界浏览器
逐项查看什么被信任，什么不被信任。
点击每个节点，查看它的作用、产出以及仍需进行的检查。
UNTRUSTED
CHECKED
重要边界
NPA 目前不是 Lean 或 Rocq 的实用替代品。本页说明以证书为中心的研究设计，并不保证商业系统没有 bug，也不保证自动定理求解。
证书检查 / 说明用模拟
体验证书被检查的流程。
浏览器中的交互用于说明检查流程。它不会运行 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 |
|---|---|---|---|
| 定位 | 开源编程语言和证明辅助系统。 | 拥有长期研究历史的交互式定理证明器。 | 用于研究证书优先检查的实现仓库。 |
| 典型用途 | 数学、软件验证和编程。 | 数学、规格、程序验证和代码提取。 | 研究证明证书和独立检查。 |
| 强调点 | 可扩展性、库和交互式证明。 | 表达能力、成熟方法和库。 | 小型可信基和规范证书。 |
| 本页中的处理 | 学习、比较和互操作的参照。 | 学习、比较和形式化方法的参照。 | Finite Field 的研究项目。 |
| 边界 | 仍需要专业知识。 | 仍需要专业知识。 | 目前不作为 Lean 或 Rocq 的实用替代品。 |
研究方法
把“成功了”变成可重复的检查流程。
当别人能够在相同条件下重新运行、检查并拒绝结果时，结果才更可靠。
问题
定义需要检查的内容：性能、正确性、兼容性或范围。
假设
在评价前写明假设、排除项、公理、数据缺口和偏差。
成果物
保留源、证书、输入、执行日志和哈希。
独立检查
通过不同于生成侧的路径检查结果。
基准
固定硬件、版本、时间限制、实例集和随机种子。
边界
公开失败、未支持案例、性能边界和下一步验证。
可复现性构建器
检查研究发布还缺少什么。
该清单只在浏览器中处理。它不是认证分数。
准备度
0%下一步
先定义研究问题和成功条件。在决定成果物格式前，先固定需要比较或检查的内容。
公开成果物
从一个入口追踪公开成果物。
本页不进行运行时 GitHub API 调用。仓库状态是已复核的快照，发布前必须再次确认。
4 个成果物
finitefield-org
npa
证书优先的证明工具链
Rust / OCamlApache-2.0Experimental
打开
finitefield-org
npa-std
标准定理包
ProofsPackageExperimental
打开
finitefield-org
npa-mathlib
形式化数学库
MathematicsProofsResearch
打开
GitHub
finitefield-org
公开仓库索引
OrganizationOpen source
打开
没有匹配的公开成果物。
发布方针
公开仓库、研究笔记和基准应包含检查日期、成熟度、复现步骤和已知限制。星标数和提交数不作为研究质量信号展示。
从 Lab 到业务现场
把研究纪律带入业务系统设计。
并不是每个客户系统都需要定理证明。真正有用的迁移，是明确哪些部分必须被信任、比较、检查、修正，并由人最终批准。
Lab 方法
把生成、计算和最终检查分开，而不是同等信任每一层。
把输入、输出、证书、哈希和日志保留下来，作为可复查的成果物。
在比较结果之前，先固定数据、版本、命令和评价条件。
约束、失败案例和未解决事项，应和结果一样被清楚公开。
客户系统
定义谁输入、谁复核、谁覆盖修改、谁确认结果。
显示约束、评价分数、被拒候选和未解决事项。
保留条件变更、计算运行和最终批准记录。
让自动输出可以被操作人员修正、拒绝和说明。
研究笔记
让更新历史和证据保持可读。
并非每张卡都是已发布文章。准备中的笔记在获得日期、来源和复现步骤前，不标记为已发布工作。
NPA / Current
为什么把证书放在中心
说明为什么最终证据应是由小型独立路径检查的标准化证书。
查看公开仓库Design note / planned
让优化结果可以被说明
关于在 UI 中公开目标、硬约束、软偏好和未解决分配的设计笔记。
查看相关演示Benchmark / planned
公平比较求解器的条件
计划中的笔记，内容包括实例集、时间限制、最优性差距、随机种子和硬件。
查看发布标准“准备中”项目不是已发布文章。发布后，每篇笔记都需要日期、来源、作者、复现路径和已知限制。
01 Math Lab 是合同开发服务吗？
不是。这里用于发布研究态度和成果物。在客户讨论中，我们会区分可应用的方法、还需要验证的方法，以及仍处于研究阶段的主题。
02 NPA 能替代 Lean 或 Rocq 吗？
不能。当前 NPA 不是 Lean 或 Rocq 的实用替代品。它是围绕证书、独立检查和小型可信基的研究与实现项目。
03 你们会直接信任 AI 生成的证明吗？
不能直接信任。AI、搜索和 tactic 可以帮助生成候选。我们关注的是最终证书是否被独立于生成路径的检查器接受。
04 形式化验证能消除所有 bug 吗？
不会。形式化方法会针对明确规格检查特定性质。错误规格、范围外代码、运行操作和外部服务仍需要单独审查。
05 这和业务系统开发有关吗？
相关。我们通常逐步应用这种纪律：约束、结果原因、计算历史、权限边界，以及重要业务逻辑的检查。
来源快照 / 2026-06-21
NPA 相关主张基于 finitefield-org/npa 仓库快照。Lean 和 Rocq 的定位基于其官方网站。仓库状态、最新标签和方法复核表述已于 2026-06-28 确认；M10-T14 仍需发布前最终 readback。