Finite Field / Математическа лаборатория

Изграждайте доказателства за коректност, а не само бързи резултати.

Математическата лаборатория е мястото, където показваме как подхождаме към математическото моделиране, доказването на теореми, формалната проверка, възпроизводимостта и доверената реализация, без да преувеличаваме доказателствата.

Вижте изследователските области Отворете страницата за NPA

Публични проекти: NPA / STD / MATHLIB
Основен език: Rust
Версия на NPA: v0.1.1

Доказателен одит / концептуален поглед Само за четене

01 канонични байтове / формат OK

02 хеш на сертификата OK

03 проверка на зависими доказателства OK

04 присъда без изходен код OK

Видима граница на доверие

Тази страница не твърди, че NPA е практически заместител на Lean или Rocq, а симулацията в браузъра не изпълнява NPA.

Принципът на лабораторията

Публикувайте не само резултатите, но и границите на проверката.

Заключение като „проработи“, „беше бързо“ или „беше доказано“ не е достатъчно. Показваме поотделно входните данни, допусканията, доверените части, независимо проверимите артефакти и нерешените въпроси.

01 / Граница

Дръжте доверителната база малка.

Не поставяйте сложните генератори или изкуствения интелект в центъра на доверието. Посочете ясно малката проверяваща страна.

02 / Доказателства

Превърнете доказателствата в артефакт

Оставяйте сертификатите, хешовете, списъците с предположения, условията за бенчмарк и журналите във форма, която други могат да проверят.

03 / Възпроизвеждане

Проектирайте за възпроизводимост

Фиксирайте инструменталните вериги, входните данни, командите за изпълнение и критериите, така че резултатът да може да се провери отново.

04 / Честност

Не преувеличавайте състоянието на научните изследвания.

Покажете практически методи, експерименти и изследвания поотделно.

ПРЕГЛЕД НА МЕТОДА

Категория за метод на услуга, която все още изисква обхват, отговорност, клиентски доказателства и одобрение, преди да се описва като готова за проект.

ЕКСПЕРИМЕНТАЛНО

Съществува работна реализация, но промени в мащаба, съвместимостта, производителността или спецификацията остават възможни.

ИЗСЛЕДВАНЕ

Проектирането, оценката, доказателството или изпълнението на проекта са в процес, но това не означава, че ще бъде комерсиално достъпно или завършено.

Изследователско портфолио

Вижте изследвания по зрелост и артефакти.

Всяка карта показва зрелост, артефакти, текущо състояние и следващо валидиране.

8 се показват

ЕКСПЕРИМЕНТАЛНО ОТВОРЕН КОД

Nano Proof Auditor

Инструментална верига за доказателства със сертификата като първи артефакт

Изследователска инструментална верига, която поставя каноничните сертификати за доказателства и малка проверяваща база в центъра на прегледа на зависими доказателства.

Артефакти: изходен код / спецификация / шаблони за CI
Текущо: публична снимка v0.1.1
Следваща проверка: външни пакети с теореми и независима проверка

Отворете детайлите за NPA

ЕКСПЕРИМЕНТАЛНО ОТВОРЕН КОД

Стандартна библиотека на NPA

Logic / Nat / List / Algebra

Стандартно хранилище с пакети от теореми за повторно използваеми основи на NPA.

Артефакти: изходен код / пакети с доказателства
Текущо: публично отделено хранилище
Следваща проверка: обхват на пакета и съвместимост

GitHub

ИЗСЛЕДВАНЕ ОТВОРЕН КОД

Математическа библиотека на NPA

Формална математическа библиотека

Насока за библиотека, която съхранява математически теореми като самостоятелно проверими доказателства.

Артефакти: изходен код / пакети с доказателства
Текущо: публично хранилище в разработка
Следваща проверка: структура на библиотеката и одит на зависимостите

GitHub

ПРЕГЛЕД НА МЕТОДА МЕТОД

Модели за планиране с ограничения

Планиране / маршрутизация / назначение

Метод за разграничаване на твърдите ограничения и критериите за оценка при смени, посещения, маршрути, производство и разпределяне.

Артефакти: модел / прототип / обяснителен отчет
Текущо: метод за услуга; публичното твърдение е ограничено до преглед на метода
Следваща проверка: клиентски доказателства и одобрение на обхвата

Вижте прототип

ИЗСЛЕДВАНЕ ИЗМЕРВАНЕ

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

Бенчмарк и доказателства

Програма за фиксиране на набори от инстанции, хардуер, времеви ограничения, случайни семена и сурови журнали, преди да се правят твърдения за ефективност.

Артефакти: регистър на бенчмаркове / сурови журнали / отчет
Текущо: дизайн на изследователска програма
Следваща проверка: първи публичен корпус за бенчмарк

Вижте метода

ИЗСЛЕДВАНЕ ФОРМАЛНИ МЕТОДИ

Проверка на критичната бизнес логика

Инварианти за бизнес системи

Изследване за разделяне на такси, разрешения, инвентар и преходи на състояния в спецификации и инварианти.

Артефакти: спецификация / инварианти / тестов или доказателствен отчет
Текущо: проучване на обхвата
Следваща проверка: избор на един ограничен случай, близък до продукционна среда

Преглед на дизайна на сигурността

ЕКСПЕРИМЕНТАЛНО ИНЖЕНЕРИНГ

Малки доверени компоненти в Rust

Малки надеждни компоненти

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

Артефакти: ядро на NPA / пакет за сертификати / референтен проверител
Текущо: публична реализация в NPA
Следваща проверка: съвместимост с независим проверител

Вижте изходния код

ИЗСЛЕДВАНЕ ИИ × ДОКАЗАТЕЛСТВА

Подпомагане и независима проверка на ИИ

Създавайте свободно, проверявайте строго

Изследователска посока, която оставя ИИ да генерира кандидати, докато окончателните доказателства се проверяват независимо.

Артефакти: генератор на кандидати / сертификат / отчет от проверител
Текущо: изследователска посока, съвместима с модела на доверие на NPA
Следваща проверка: измерен процес за авторство

Вижте границата на доверието

Не е открита подходяща област за изследване.

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

Nano Proof Auditor

Отделете генерирането на доказателства от това, на което вярваме.

NPA е инструментална верига за зависими доказателства със сертификата като първи артефакт. Потребителски интерфейси, тактики, търсене на теореми, плъгини, ИИ, изходни файлове и статус на CI могат да помагат за създаване на кандидати, но не са довереното доказателство.

ЕКСПЕРИМЕНТАЛНООТВОРЕН КОДAPACHE-2.0

Текуща снимка

v0.1.1

Публичната информация е проверена на 2026-06-21.

Основно ядро

Rust

Rust верификаторът и ядрото са част от страната на проверката.

Артефактът на одита

.npcert

Каноничните байтове на сертификата са обектът за проверка.

Точка за повторна проверка

ръчен преглед

Състоянието на хранилището и видимостта на пакетите трябва да бъдат преразгледани преди публикуването.

Изследовател на границите на доверие

Преминете през това на какво може и на какво не може да се вярва.

Изберете всеки възел, за да проверите какво прави, какво произвежда и коя проверка все още е необходима.

НЕДОВЕРЕНО

ПРОВЕРЕНО

Недоверен / кандидат

ИИ и търсене на теореми

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

Вход: Цели, предположения, известни теореми, изходни файлове
Изход: Доказателства за кандидатите и пътища за търсене.
Необходими проверки: Преобразуване на канонични сертификати и независима проверка

Важна граница

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

Проверка на сертификат / обяснителна симулация

Проследете потока на проверка на сертификата.

Взаимодействието в браузъра обяснява потока на проверка. То не изпълнява NPA, Rust, WASM или истински сертификати за доказателства.

Пример за CLI

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

NPA / одитна следа ГОТОВО

01 Прочетете сертификата.канонични байтове / формат ИЗЧАКВАНЕ
02 Проверете хеша на сертификатахеш на сертификата ИЗЧАКВАНЕ
03 Проверете с ядротопроверка на зависими доказателства ИЗЧАКВАНЕ
04 Проверете повторно с референтния проверителприсъда без изходен код ИЗЧАКВАНЕ
05 Сравнете доклада за аксиомитехеш на отчета за аксиомите ИЗЧАКВАНЕ

Вердикт

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

Стартирайте обяснението, за да видите стъпките по ред.

Екосистема за доказателства

Пояснявайте ролите вместо инструментите за класиране.

Lean и Rocq са зрели екосистеми за асистирано доказване. NPA е представен тук като изследователски и внедрителски проект, съсредоточен върху сертификати, а не като заместител.

Предмет	Lean	Rocq	NPA
Позиция	Език за програмиране с отворен код и асистент за доказване.	Интерактивен доказвач на теореми с дълга изследователска история.	Изследователско и внедрителско хранилище за проверка със сертификата като първи артефакт.
Типично използване	Математика, проверка на софтуера и програмиране.	Математика, спецификации, проверка на програмата и извличане.	Изследване на сертификати за доказателство и независима проверка.
Акцент	Разширяемост, библиотеки и интерактивно доказателство.	Експресивност, зрели методи и библиотеки.	Малка надеждна база и канонични сертификати.
Как тази страница го третира	Референция за обучение, сравнение и оперативна съвместимост.	Референция за методи за обучение, сравнение и формализация.	Изследователски проект на Finite Field.
Граница	Все още са необходими специализирани знания.	Все още са необходими специализирани знания.	Засега не е предназначен за практическа замяна на Lean или Rocq.

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

Изследователски метод

Превърнете „проработи“ в повтаряема процедура за проверка.

Резултатът става по-силен, когато някой може да го повтори, да го прегледа и да го отхвърли при същите условия.

Въпрос

Определете какво трябва да се провери: производителност, точност, съвместимост или обхват.

Предположения

Запишете предположенията, изключенията, аксиомите, пропуските в данните и отклоненията преди оценката.

Артефакт

Съхранявайте изходния код, сертификатите, входните данни, журналите от изпълнение и хешовете.

Независима проверка

Проверявайте резултатите чрез различен път от поколението.

Бенчмарк

Фиксирайте хардуера, версиите, времевите ограничения, наборите от инстанции и случайните семена.

Ограничения

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

Конструктор за възпроизводимост

Проверете какво все още липсва в научноизследователска публикация.

Контролният списък се обработва само в браузъра. Това не е резултат от проверка на сертификат.

Готовност

Въпрос за изследване и условие за успехКакво се смята за успех или провал. Фиксирани инструменти и зависимостиВерсии, файлове за блокиране, хардуер и среда. Входящи данни или процес на генериранеАнонимизация, лиценз, източник и хеш. Командна последователност за повторно изпълнениеОт инициализацията до генерирането на резултати. Проверими артефакти и сурови журналиСертификати, доклади, регистри и хеши. Ограничения, неуспехи и отворени въпросиНеподдържани случаи и нерешени въпроси.

Следващото действие

Определете първо въпроса за изследването и условието за успех.

Преди да решите формати на артефакта, определете какво ще бъде сравнено или проверено.

Публични артефакти

Следете публичните артефакти от един вход.

Статусът на хранилищата е прегледана снимка и трябва да се провери преди публикуване.

4 артефакти

finitefield-org

npa

Инструментална верига за помощ при доказване и проверка със сертификата като първи артефакт.

Rust / OCamlApache-2.0Експериментално

ПРОВЕРКА проверка на пакети със сертификати

finitefield-org

npa-std

Пакет със стандартни теореми

ДоказателстваПакетЕкспериментално

РОЛЯ Std.Logic / Nat / List

finitefield-org

npa-mathlib

Формална математическа библиотека

МатематикаДоказателстваИзследване

РОЛЯ формални пакети с теореми

GitHub

finitefield-org

Индекс на публичните хранилища

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

ИНДЕКС всички публични хранилища

Никой публичен артефакт не отговаря на търсенето.

Политика за публикуване

Публичните хранилища, изследователските бележки и бенчмарковете трябва да съдържат проверена дата, срок на валидност, стъпки за възпроизвеждане и известни ограничения.

От лабораторията до операциите

Доведете научната дисциплина в дизайна на бизнес системи.

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

Лабораторната практика

Граници на доверие

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

Доказателства

Съхранявайте входовете, изходите, сертификатите, хешовете и журналите като артефакти, които могат да се преглеждат.

Възпроизводимост

Фиксирайте данните, версиите, командите и критериите за оценка, преди да сравнявате резултатите.

Ограничения

Публикувайте ограниченията, неуспешните случаи и нерешените въпроси със същата тежест като резултатите.

Клиентска система

Правомощия и отговорност

Определете кой въвежда, кой преглежда, кой прехвърля и кой потвърждава резултата.

Причини за решението

Покажете ограниченията, оценките, отхвърлените кандидати и нерешените точки.

Аудитоспособност

Запазете промените в условията, изчисленията и историята на окончателното одобрение.

Човешка преценка

Направете автоматичния резултат коригируем, отхвърляем и обясним за операторите.

01 Смени и персонал

Покажете нарушенията на правилата и удовлетвореността от предпочитанията поотделно.

02 Маршрутизиране на превозни средства

Дръжте видими причините за маршрута, капацитета, времевите прозорци и изключенията.

03 Производствено планиране

Обяснявайте непланираната работа, тесните места и компромисите при пренастройване.

04 Разпределяне и съпоставяне

Показвайте причините за предложения вариант и алтернативите преди одобрение.

Изследователски бележки

Дръжте историята на обновяване и доказателствата лесни за четене.

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

NPA / текущо2026.06.21

Защо да поставяте сертификатите в центъра?

Защо окончателното доказателство трябва да бъде стандартизиран сертификат, проверен от малък независим път.

Виж публичния репозиторий

Проектна бележка / планираноПодготвяне

Как да направим резултатите от оптимизацията обясними

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

Вижте свързаните демонстрации

Бенчмарк / планираноПодготвяне

Условия за честно сравнение на решатели

Планирана бележка за набори от инстанции, времеви ограничения, разлики до оптимума, случайни семена и хардуер.

Вижте критериите за публикуване.

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

ЧЗВ

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

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

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

01 Математическата лаборатория услуга за договорна разработка ли е?

Не. Това е място за публикуване на изследователския подход и артефактите. В разговорите с клиенти отделяме приложимите методи, методите, които се нуждаят от допълнителна проверка, и темите на изследователски етап.

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

Не. Настоящият NPA не е практически заместител на Lean или Rocq. Това е изследователски и внедрителски проект за сертификати, независима проверка и малка доверена база.

03 Доверявате ли се на доказателства, генерирани от ИИ, без допълнителна проверка?

Не. ИИ, търсенето и тактиките помагат да се генерират кандидати. Ние се фокусираме върху това дали окончателният сертификат се приема от проверител, независим от тези пътища за генериране.

04 Дали официалната проверка премахва всички бъгове?

Не. Формалните методи проверяват конкретни свойства спрямо изрична спецификация. Грешни спецификации, код извън обхвата, операции и външни услуги все още изискват отделен преглед.

05 Има ли нещо общо с работата на бизнес системата?

Обикновено прилагаме дисциплината постепенно: ограничения, причини за резултата, история на изчисленията, граници на разрешенията и проверки за важна бизнес логика.

Обсъдете проблем

Можете да обсъдите работата, която трябва да се реши, а не само изследователската тема.

Започнете от текущата електронна таблица, правилата и местата, където хората коригират решенията. Така можем да подредим дали първо са нужни математическо моделиране, автоматизация на правилата или прототип.

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

Снимка на източниците / 2026-06-21

Твърденията за NPA се основават на снимката на хранилището finitefield-org/npa. Позиционирането на Lean и Rocq се основава на техните официални сайтове.