Публичен статус
Изследователско и развойно хранилище
GitHub хранилището е публично, но тази страница описва изследователско и развойно хранилище, а не внедрена услуга.
Обратно към Математическата лаборатория
NPA / Проверка на доказателства чрез сертификати
NPA: покажете границата на доказателствата, преди да се доверите на резултата.
Тази страница пресъздава раздела за NPA от Математическата лаборатория като самостоятелна страница с доказателства: публичен статус, модел на доверие, конвейер за доказване, регистър на твърденията, хранилища, източници и изрично уточнение, че NPA не е заместител.
- Публичен статус
- Изследователско хранилище
- Представя се като изследователска и развойна работа, а не като услуга за производствена гаранция.
- Публична повторна проверка
- 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 на 02.07.2026 г.
Публична повторна проверка: 02.07.2026 г. Най-новият git таг на хранилището NPA е v0.2.0; npa-std е v0.1.0; npa-mathlib е v0.1.30. Фиксираните версии в README на пакетите са показани като специфичен за хранилището контекст и не се обединяват в едно твърдение за версията на NPA.
Публичен статус
Посочете кое е публично, кое е доказателство и кога е проверено отново.
Тази страница показва основата си: локална моментна снимка на фактите, публичен източник в хранилище и датата на окончателната проверка преди стартиране.
Публична повторна проверка
2026-07-02
Повторната проверка на публичните източници приключи на 02.07.2026 г. Първоначалната реконструкция на източниците все още използва локалната моментна снимка на фактите от 21.06.2026 г.
Доказателства
Сертификати и хешове
Моментната снимка на източниците записва каноничен .npcert, certificate_hash, export_hash, axiom_report_hash и присъдите на проверяващите инструменти.
Лиценз
Apache-2.0 проверен
Apache-2.0 беше проверен за npa, npa-std и npa-mathlib чрез публичните метаданни в LICENSE на 02.07.2026 г.
Граница
NPA не е практичен заместител на Lean или Rocq. Симулацията за инспекция в браузъра не изпълнява самия NPA. Публичните тагове, лицензът и видимостта на хранилищата бяха проверени на 02.07.2026 г. за окончателната проверка преди публикуване.
Граница на доверие
Премествайте през границата на доказателствата само каноничен сертификат.
Границата не зависи от това кой инструмент изглежда сложен. Тя определя на кой артефакт е позволено да стане доказателство след независима проверка.
Парсерът, елабораторът, тактиките, автоматизацията, търсенето на теореми, приставките, системите с ИИ, изходните файлове, файловете за повторение, индексите на теореми, плановете за публикуване, CI статусът, страниците с издания и метаданните на регистъра остават от недоверената страна на кандидатите.
Конвейер за доказване / обяснителна симулация
Покажете точния конвейер от байтовете на сертификата до доказателствата от проверката.
Симулацията в браузъра не изпълнява самия NPA, Rust, WASM или реални сертификати за доказателства. Тя визуализира реда на проверката без изходен код, който реалните артефакти трябва да удовлетворят.
CLI път за доказателствата
npa package verify-certs --root . --checker reference --json
NPA / одитна следа
ГОТОВО
- 01 Формат на сертификатаканонични .npcert байтове / сертификат, годен за парсване / проверка на формата ИЗЧАКВАНЕ
- 02 Хеш на сертификатабайтове на сертификата / хеш на сертификата / детерминиран дайджест ИЗЧАКВАНЕ
- 03 Присъда на ядротосертификат / приемане или отхвърляне / отчет от Rust проверителя ИЗЧАКВАНЕ
- 04 Референтен проверителсертификат, фиксиран по хеш / независимо приемане или отхвърляне / отчет от проверител без изходен код ИЗЧАКВАНЕ
- 05 Отчет за аксиомитепроверен пакет / хеш на отчета за аксиомите / инвентар на допусканията ИЗЧАКВАНЕ
Вердикт
Обяснителният конвейер още не е стартиран.Стартирайте обяснението, за да маркирате последователно пътя за проверка без изходен код.
Регистър на твърденията
Разделяйте доказателствата, чувствителните към времето факти и твърденията за границите.
Страницата не разчита на свободен изследователски текст. Всяко публично твърдение е свързано с локална моментна снимка на фактите, източник и действие преди публикуване.
| Твърдение | Публична формулировка | Статус | Източник | Действие преди публикуване |
|---|---|---|---|---|
| CL-001 | NPA поставя сертификата на първо място: проверимата граница е каноничният артефакт .npcert и пътят за проверка около него. | Проверено публично твърдение | S01 / 2026-07-02 | Прегледайте отново при промяна на README. |
| CL-002 | Публичната повторна проверка от 02.07.2026 г. установи, че най-новият git таг на хранилището NPA е v0.2.0. README файловете на свързаните пакети все още показват специфични за хранилищата фиксирани версии, затова формулировката за версията остава ограничена до съответното хранилище. | Проверено чрез публична повторна проверка | S01 / S02 / 2026-07-02 | Ограничете формулировката за тага до съответното хранилище. |
| CL-003 | Локалната моментна снимка на фактите записва фиксирана версия на инструменталната верига Rust 1.95.0; тя не се използва като маркетингово твърдение. | Проверено, чувствително към времето | S01 / 2026-07-02 | Проверете отново, ако се показва версията на инструменталната верига. |
| CL-004 | NPA не е практичен заместител на Lean или Rocq. Тази граница трябва да остава видима при всяко сравнение. | Проверено твърдение за границата | S01 / S03 / S05 / 2026-07-02 | Запазете уточнението. |
| CL-005 | npa-std и npa-mathlib са отделни публични хранилища за пакети с теореми в организацията finitefield-org. | Проверено публично твърдение | S01 / S02 / 2026-07-02 | Проверете отново видимостта на хранилищата, ако публикуването се забави или хранилищата се променят. |
| CL-006 | Хранилищата npa, npa-std и npa-mathlib публикуват лиценз Apache-2.0 чрез своите публични метаданни в LICENSE. | Проверено публично твърдение | S01 / S02 / 2026-07-02 | Проверете файла LICENSE отново при основно издание. |
Хранилища и лиценз
Показвайте ясно кода, хранилищата на пакетите и видимостта на организацията.
Връзките към хранилищата сочат към публични източници, но не гарантират, че тази страница е синхронизирана с най-новото състояние в GitHub.
4 показани хранилища
finitefield-org
npa
Инструментална верига за асистиране и проверка на доказателства, поставяща сертификата на първо място.
- Лиценз
- Apache-2.0 е проверен от файла LICENSE на 02.07.2026 г.
- Проверка
- Най-нов git таг: v0.2.0. Няма публикувано най-ново GitHub издание. Текуща препратка към инструменталната верига в README: NPA_GIT_TAG=v0.2.0.
експерименталноRust / OCamlсертификатът е първи
Отваряне на хранилището
finitefield-org
npa-std
Хранилище със стандартен пакет от теореми за изходни доказателства на NPA.
- Лиценз
- Apache-2.0 е проверен от файла LICENSE на 02.07.2026 г.
- Проверка
- Най-нов git таг и GitHub издание: v0.1.0. Версия на метаданните на пакета в README: 0.1.0; фиксирана версия на инструменталната верига за пакета: NPA_GIT_TAG=v0.1.1.
експерименталнопакет с теоремиизточник на доказателства
Отваряне на хранилището
finitefield-org
npa-mathlib
Изследователско хранилище за библиотека по формална математика.
- Лиценз
- Apache-2.0 е проверен от файла LICENSE на 02.07.2026 г.
- Проверка
- Най-нов git таг: v0.1.30. Най-ново GitHub издание: v0.1.9. Версия на метаданните на пакета в README: 0.2.1; фиксирана версия на инструменталната верига за пакета: NPA_GIT_TAG=v0.1.1.
изследванеформална математикабиблиотека
Отваряне на хранилището
finitefield-org
GitHub организация на Finite Field
Публична моментна снимка на организацията за семейството хранилища на Лабораторията.
- Лиценз
- Прилагат се специфични за хранилищата лицензи
- Проверка
- npa, npa-std и npa-mathlib са публични според повторната проверка чрез GitHub API от 02.07.2026 г.
публичен индексснимка на видимосттаизходен код
Отваряне на организацията
Нито едно хранилище не съответства на текущото търсене.
GitHub хранилищата са източникът за публичния статус на кода. Лицензът, текущите тагове, публичната видимост и формулировките за изданията бяха проверени на 02.07.2026 г. като окончателна повторна проверка M10-T14.
Контрол на екосистемата за доказателства
Изяснете ролите, преди да сравнявате инструменти за доказване.
Това е таблица на ролите, а не класация. Lean и Rocq остават референтните екосистеми за асистенти за доказване; NPA е представен като изследователска и развойна работа, съсредоточена върху сертификати.
| Елемент | Lean | Rocq | NPA |
|---|---|---|---|
| Позиция | Програмен език с отворен код и асистент за доказване. | Интерактивен инструмент за доказване на теореми с дълга изследователска история. | Изследователско и развойно хранилище за проверка, поставяща сертификата на първо място. |
| Типична употреба | Математика, проверка на софтуер и програмиране. | Математика, спецификации, проверка на програми и извличане. | Изследвания на сертификати за доказателства, независима проверка и малка доверена основа. |
| Граница на доказателствата | Собственото му доверено ядро и екосистема определят границата на проверката. | Собственото му ядро и проверените разработки определят границата на проверката. | Каноничният артефакт .npcert преминава от генериране към проверка. |
| Как го разглежда тази страница | Отправна точка за обучение, сравнение и оперативна съвместимост. | Отправна точка за обучение, сравнение и методи за формализация. | Изследователски проект на Finite Field, а не продуктово обещание. |
| Граница | Все още са необходими специализирани знания. | Все още са необходими специализирани знания. | Към момента NPA не е практичен заместител на Lean или Rocq. |
Източници
Публикувайте картата на източниците редом с тълкуването.
Източниците са показани, за да може читателят да различи кои твърдения идват от публични хранилища, официални сайтове на инструменти за доказване и фирмен контекст.
S01
finitefield-org/npa
Основен източник за предназначението и модела на доверие на NPA, формулировката за текущия таг v0.2.0 на хранилището, командите, структурата на хранилището и лиценза.
Отваряне на източника S02GitHub организация на Finite Field
Основен източник за публичната видимост на хранилищата, най-новите git тагове, страниците с издания и моментната снимка на семейството хранилища на Лабораторията, проверена на 02.07.2026 г.
Отваряне на източника S03Официален сайт на Lean
Основен източник за публичното позициониране на Lean, проверен на 02.07.2026 г.
Отваряне на източника S04Справочник на езика Lean
Основен източник за контекста на зависимата теория на типовете и референтното ядро, проверен на 02.07.2026 г.
Отваряне на източника S05Официален сайт на Rocq Prover
Основен източник за публичното позициониране на Rocq, проверен на 02.07.2026 г.
Отваряне на източника S06Фирмен сайт на FINITE FIELD
Фирмен източник за марката Finite Field и бизнес контекста.
Отваряне на източникаЧЗВ
Статус на NPA и граници на проверката.
Отговорите подчертават доверената граница, преди читателите да объркат изследователска страница с внедрена услуга за асистирано доказване.
Научете повече за компанията01 Тази страница представлява ли продуктова гаранция?
Не. Тук NPA е показан като изследователско и развойно хранилище.
02 Може ли NPA да замени Lean или Rocq?
Не. NPA не е практичен заместител на Lean или Rocq.
03 Страницата изпълнява ли реална NPA проверка?
Не. Симулацията в браузъра не изпълнява самия NPA, Rust, WASM или реални сертификати за доказателства.
04 Какво се счита за доказателство тук?
Сертификатният артефакт, детерминираните хешове, резултатът от Rust ядрото/проверителя, резултатът от референтната проверка без изходен код и отчетът за аксиомите образуват доказателствата от страната на проверката.
05 Кои факти се нуждаят от повторна проверка?
Текущата публична версия, видимостта на хранилищата, фиксираните версии на инструменталната верига, текстът на лиценза и формулировките на източниците бяха проверени отново на 02.07.2026 г.
От дисциплината на доказването към операциите
Прилагайте същата дисциплина към доказателствата, когато едно бизнес решение трябва да заслужава доверие.
За бизнес системите полезният урок не е навсякъде да се добавя доказване на теореми. Той е да се реши какво трябва да бъде генерирано, проверено, записано, коригирано и одобрено от хора.