NPA / Certificate-first proof checking

NPA: покажете границата на proof evidence преди да се доверите на резултат.

Тази страница реконструира секцията NPA от Math Lab като самостоятелна evidence page: публично състояние, trust model, proof pipeline, claim register, repositories, sources и яснота, че не е заместител.

Прегледайте границата на доверие Отворете GitHub хранилището

Публично състояние: Изследователско хранилище; Показано като изследване и реализация, не като производствена услуга за гарантиране.
Публична повторна проверка: 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; Apache-2.0 е проверен за npa, npa-std и npa-mathlib на 2026-07-02.

Публична повторна проверка: 2026-07-02. Последният git tag на NPA е v0.2.0; npa-std е v0.1.0; npa-mathlib е v0.1.30. README pins се показват като контекст за отделните хранилища и не се сливат в едно твърдение за версия на NPA.

Преглед на NPA evidence page с certificate checking и trust-boundary inspection — Визуализацията е статичен преглед на резултат от certificate-checking и обяснение на trust boundary. Тя не е live NPA trace.

Public status

Посочете кое е публично, кое е доказателство и кога е проверено.

Тази страница показва основата си: локална truth snapshot, публичен repository source и дата на final prelaunch readback.

Публично състояние

Изследователско хранилище

GitHub хранилището е публично, но тази страница описва изследователско и инженерно хранилище, не внедрена услуга.

Public recheck

2026-07-02

Public-source readback е завършен на 2026-07-02. Оригиналната reconstruction на source все още използва локалната truth snapshot от 2026-06-21.

Evidence

Certificates and hashes

Source snapshot записва canonical .npcert, certificate_hash, export_hash, axiom_report_hash и checker verdicts.

License

Apache-2.0 verified

Apache-2.0 е проверен за npa, npa-std и npa-mathlib чрез public LICENSE metadata на 2026-07-02.

Boundary

NPA не е практичен заместител на Lean или Rocq. Разпространената browser inspection simulation не изпълнява NPA. Public tags, license и repository visibility са проверени на 2026-07-02 за final publication readback.

Trust boundary

Преместете само canonical certificate през evidence boundary.

Границата не е въпрос кой tool изглежда сложен. Въпросът е кой artifact може да стане evidence след independent checking.

Parser, elaborator, tactics, automation, theorem search, plugins, AI systems, source files, replay files, theorem indexes, publish plans, CI status, release pages и registry metadata остават от untrusted candidate side.

Proof pipeline / обяснителна симулация

Покажете точния pipeline от certificate bytes до checking evidence.

Браузърната симулация не изпълнява NPA, Rust, WASM или реални proof certificates. Тя визуализира реда на source-free checking, който реалните artifacts трябва да удовлетворят.

CLI evidence path

npa package verify-certs --root . --checker reference --json

NPA / audit trace READY

01 Certificate formatcanonical .npcert bytes / parseable certificate / format check WAIT
02 Certificate hashcertificate bytes / certificate_hash / deterministic digest WAIT
03 Kernel verdictcertificate / accept or reject / Rust verifier report WAIT
04 Reference checkerhash-pinned certificate / independent accept or reject / source-free checker report WAIT
05 Axiom reportchecked package / axiom_report_hash / assumption inventory WAIT

Verdict

Обяснителният pipeline още не е стартиран.

Стартирайте обяснението, за да маркирате source-free checking path по ред.

Claim register

Разделяйте доказателствата, чувствителните във времето факти и граничните твърдения.

Страницата не разчита на свободен изследователски текст. Всяко публично твърдение е свързано с локална снимка на истината, източник и действие за публикуване.

Твърдение	Публична формулировка	Състояние	Източник	Действие преди публикуване
CL-001	NPA е certificate-first: одитируемата граница е canonical .npcert artifact и проверяващият път около него.	Проверено публично твърдение	S01 / 2026-07-02	Публична повторна проверка при промяна в README.
CL-002	Повторната проверка от 2026-07-02 намери последния git tag на NPA repository като v0.2.0. README pins остават по repository, затова version wording остава ограничен по repository.	Проверена публична повторна проверка	S01 / S02 / 2026-07-02	Ограничете tag wording по repository.
CL-003	Локалният truth snapshot записва Rust 1.95.0 toolchain pin; той не се използва като marketing claim.	Проверено, чувствително във времето	S01 / 2026-07-02	Проверете отново само ако се показва toolchain version.
CL-004	NPA не е практичен заместител на Lean или Rocq. Тази граница трябва да остане видима при всяко сравнение.	Проверено гранично твърдение	S01 / S03 / S05 / 2026-07-02	Запазете disclaimer.
CL-005	npa-std и npa-mathlib са отделни public theorem-package repositories в finitefield-org organization.	Проверено публично твърдение	S01 / S02 / 2026-07-02	Проверете repository visibility отново при забавена публикация или промени.
CL-006	npa, npa-std и npa-mathlib показват Apache-2.0 licensing чрез public LICENSE metadata.	Проверено публично твърдение	S01 / S02 / 2026-07-02	Проверете LICENSE при major release.

Repositories and license

Дръжте явни кода, package repositories и organization visibility.

Repository links са указатели към публичен source, не гаранция, че текущата страница е синхронизирана с последното състояние в GitHub.

4 показани хранилища

finitefield-org

npa

Инструментална верига за certificate-first proof assistance и verification.

License: Apache-2.0 е проверен от LICENSE на 2026-07-02.
Verification: Latest git tag: v0.2.0. No latest GitHub release is published. README current toolchain reference: NPA_GIT_TAG=v0.2.0.

experimentalRust / OCamlcertificate-first

Отвори хранилище

finitefield-org

npa-std

Стандартно theorem package repository за NPA proof sources.

License: Apache-2.0 е проверен от LICENSE на 2026-07-02.
Verification: Последен git tag и GitHub release: v0.1.0. README package metadata version: 0.1.0; package toolchain pin: NPA_GIT_TAG=v0.1.1.

experimentaltheorem packageproof source

Отвори хранилище

finitefield-org

npa-mathlib

Изследователско repository за formal mathematics library.

License: Apache-2.0 е проверен от LICENSE на 2026-07-02.
Verification: Последен git tag: v0.1.30. Последен GitHub release: v0.1.9. README package metadata version: 0.2.1; package toolchain pin: NPA_GIT_TAG=v0.1.1.

researchformal mathematicslibrary

Отвори хранилище

finitefield-org

Finite Field GitHub organization

Публична organization snapshot за Lab repository family.

License: Прилагат се license условията на отделното repository
Verification: npa, npa-std и npa-mathlib са публични към GitHub API readback от 2026-07-02.

public indexvisibility snapshotsource

Отвори организация

GitHub хранилищата са source за публичното състояние на кода. License, current tags, public visibility и release wording са проверени на 2026-07-02 като M10-T14 final readback.

Proof ecosystem guard

Изяснете ролите преди сравнение на proof tools.

Това е таблица на ролите, не класация. Lean и Rocq остават референтни екосистеми за proof assistant; NPA е представен като изследователска и инженерна работа, центрирана върху сертификати.

Елемент	Lean	Rocq	NPA
Позиция	Open-source programming language и proof assistant.	Interactive theorem prover с дълга изследователска история.	Research and implementation repository за certificate-first checking.
Типична употреба	Mathematics, software verification и programming.	Mathematics, specifications, program verification и extraction.	Research into proof certificates, independent checking и малка trusted base.
Граница на доказателствата	Собственият trusted kernel и ecosystem определят checking boundary.	Собственият kernel и checked developments определят checking boundary.	Canonical .npcert artifact преминава от generation към checking.
Как тази страница го третира	Референция за learning, comparison и interoperability.	Референция за learning, comparison и formalization methods.	Finite Field research project, не product promise.
Граница	Все още са нужни специализирани знания.	Все още са нужни специализирани знания.	В момента NPA не е практичен заместител на Lean или Rocq.

Официален сайт на Lean Официален сайт на Rocq Prover NPA GitHub

Sources

Публикувайте source map до интерпретацията.

Източниците са показани, за да се вижда кои твърдения идват от публични хранилища, официални proof-tool сайтове и фирмен контекст.

S01

finitefield-org/npa

Primary source за NPA purpose, trust model, v0.2.0 current repository tag wording, commands, repository layout и license.

Отвори източник S02

Finite Field GitHub organization

Primary source за public repository visibility, latest git tags, release pages и Lab repository family snapshot checked on 2026-07-02.

Отвори източник S03

Lean official site

Primary source за public positioning на Lean, checked on 2026-07-02.

Отвори източник S04

Lean language reference

Primary source за dependent type theory и kernel reference context, checked on 2026-07-02.

Отвори източник S05

Rocq Prover official site

Primary source за public positioning на Rocq, checked on 2026-07-02.

Отвори източник S06

FINITE FIELD company site

Company source за Finite Field brand и business context.

Отвори източник

FAQ

Състояние на NPA и граници на проверката.

Отговорите поставят границата на доверие преди читателите да объркат изследователска страница с внедрена proof-assistant услуга.

Прочетете за компанията

01 Тази страница product guarantee ли е?

Не. NPA е показан тук като research and implementation repository. Client projects все още се нуждаят от отделни requirements, risk, responsibility и acceptance criteria.

02 Може ли NPA да замени Lean или Rocq?

Не. NPA не е practical replacement за Lean или Rocq. Страницата пази тази boundary visible, защото тя е важна за expectations.

03 Страницата изпълнява ли real NPA verification?

Не. Browser simulation не изпълнява NPA itself, Rust, WASM или real proof certificates. Тя обяснява inspection order.

04 Какво се брои за evidence тук?

Certificate artifact, deterministic hashes, Rust kernel/verifier result, source-free reference checker result и axiom report формират checking-side evidence.

05 Кои факти се нуждаят от rechecking?

Current public version, repository visibility, toolchain pins, license text и source wording са rechecked на 2026-07-02 и трябва да се recheck при publication delay или repository changes.

От дисциплина на доказване към операции

Използвайте същата дисциплина на доказателствата, когато бизнес решение трябва да е надеждно.

За бизнес системите полезният урок не е theorem proving навсякъде. Полезно е да се реши какво се генерира, проверява, записва, коригира и одобрява от хора.

Проверете бизнес проблема Вижте прототипа