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