Finite Field / Laboratorium matematyczne

Buduj dowody poprawności,nie tylko szybkie wyniki.

Laboratorium matematyczne pokazuje, jak traktujemy modelowanie matematyczne, dowodzenie twierdzeń, weryfikację formalną, odtwarzalność i zaufaną implementację bez wyolbrzymiania dowodów.

Zobacz obszary badań Otwórz stronę NPA

Projekty publiczne: NPA / STD / MATHLIB
Język rdzeniowy: Rust
Migawka NPA: v0.1.1

Audyt dowodu / widok koncepcyjny Tylko do odczytu

01 kanoniczne bajty / format OK

02 certificate_hash OK

03 sprawdzanie dowodu zależnego OK

04 werdykt bez źródeł OK

Widoczna granica zaufania

Ta strona nie twierdzi, że NPA jest praktycznym zamiennikiem Lean lub Rocq, a symulacja w przeglądarce nie wykonuje NPA.

Zasada laboratorium

Publikuj nie tylko wyniki, ale też granicę sprawdzania.

Samo stwierdzenie „zadziałało”, „było szybkie” albo „zostało udowodnione” nie wystarcza. Osobno pokazujemy dane wejściowe, założenia, części zaufane, artefakty możliwe do niezależnego sprawdzenia i kwestie nierozwiązane.

01 / Granica

Utrzymuj małą bazę zaufania

Nie umieszczaj złożonych generatorów ani AI w centrum zaufania. Wyraźnie pokaż małą stronę sprawdzania.

02 / Dowody

Zamień dowody w artefakt

Zostaw certyfikaty, hashe, listy założeń, warunki benchmarków i logi w formie możliwej do sprawdzenia przez innych.

03 / Odtworzenie

Projektuj pod odtwarzalność

Przypnij łańcuchy narzędzi, dane wejściowe, polecenia wykonania i kryteria, aby wynik można było sprawdzić ponownie.

04 / Uczciwość

Nie wyolbrzymiaj statusu badań

Pokazuj osobno metody praktyczne, eksperymenty i badania. Ograniczenia umieszczaj obok wyników.

PRZEGLĄD METODY

Kategoria metody usługowej, która nadal wymaga zakresu, odpowiedzialności, dowodów klienta i zatwierdzenia, zanim zostanie opisana jako gotowa do projektu.

EKSPERYMENTALNE

Istnieje działająca implementacja, ale skala, zgodność, wydajność albo zmiany specyfikacji mogą się jeszcze zmieniać. Wymagane są wersja i kroki odtworzenia.

BADANIA

Projektowanie, ocena, dowód albo implementacja są w toku. Nie oznacza to dostępności komercyjnej ani ukończenia.

Portfolio badawcze

Przeglądaj badania według dojrzałości i artefaktów.

Każda karta pokazuje dojrzałość, artefakty, obecny stan i następną walidację. Wyszukiwanie i filtry korzystają wyłącznie ze stanu po stronie przeglądarki.

8 pokazano

EKSPERYMENTALNE OTWARTY KOD

Nano Proof Auditor

Łańcuch narzędzi dowodowych oparty na certyfikatach

Badawczy łańcuch narzędzi, który umieszcza kanoniczne certyfikaty dowodu i małą bazę sprawdzania w centrum przeglądu dowodów zależnych.

Artefakty: źródło / specyfikacja / szablony CI
Obecny stan: publiczna migawka v0.1.1
Następna walidacja: zewnętrzne pakiety twierdzeń i niezależne sprawdzanie

Otwórz szczegóły NPA

EKSPERYMENTALNE OTWARTY KOD

NPA Standard Library

Logic / Nat / List / Algebra

Repozytorium standardowych pakietów twierdzeń dla ponownie używalnych podstaw NPA.

Artefakty: źródło / pakiety dowodowe
Obecny stan: publiczne repozytorium rozdzielone
Następna walidacja: zakres pakietu i zgodność

GitHub

BADANIA OTWARTY KOD

NPA Math Library

Biblioteka matematyki formalnej

Kierunek biblioteki do przechowywania twierdzeń matematycznych jako niezależnie sprawdzalnych pakietów dowodowych.

Artefakty: źródło / pakiety dowodowe
Obecny stan: publiczne repozytorium w rozwoju
Następna walidacja: struktura biblioteki i audyt zależności

GitHub

PRZEGLĄD METODY METODA

Modele planowania z ograniczeniami

Harmonogramowanie / trasy / przydziały

Metoda rozdzielania twardych ograniczeń i metryk oceny w pracy ze zmianami, wizytami, trasami, produkcją i przydziałami.

Artefakty: model / prototyp / raport wyjaśniający
Obecny stan: metoda usługowa; publiczne twierdzenie ograniczone do przeglądu metody
Następna walidacja: dowody klienta i zatwierdzenie zakresu

Zobacz prototyp

BADANIA POMIAR

Odtwarzalna ocena solverów

Benchmarki i dowody

Program ustalania zestawów instancji, sprzętu, limitów czasu, ziaren losowych i surowych logów przed twierdzeniami o wydajności.

Artefakty: rejestr benchmarków / surowe logi / raport
Obecny stan: projekt programu badawczego
Następna walidacja: pierwszy publiczny korpus benchmarkowy

Zobacz metodę

BADANIA METODY FORMALNE

Weryfikacja krytycznej logiki biznesowej

Niezmienniki systemów biznesowych

Badania nad rozdzielaniem opłat, uprawnień, zapasów i przejść stanów na specyfikacje oraz niezmienniki.

Artefakty: specyfikacja / niezmienniki / test lub raport dowodowy
Obecny stan: badanie zakresu
Następna walidacja: wybór jednego ograniczonego przypadku podobnego do produkcyjnego

Zobacz projekt bezpieczeństwa

EKSPERYMENTALNE INŻYNIERIA

Małe komponenty zaufane w Rust

Małe komponenty zaufane

Prace implementacyjne utrzymujące elementy krytyczne dla zaufania, takie jak sprawdzarki i hashe, na tyle małe, aby dało się je skontrolować.

Artefakty: jądro NPA / crate certyfikatów / sprawdzarka referencyjna
Obecny stan: publiczna implementacja w NPA
Następna walidacja: zgodność niezależnej sprawdzarki

Zobacz źródło

BADANIA AI × DOWÓD

Wsparcie AI i niezależne sprawdzanie

Generuj swobodnie, sprawdzaj rygorystycznie

Kierunek badawczy, w którym AI pomaga przy generowaniu kandydatów, a końcowy dowód jest sprawdzany niezależnie.

Artefakty: generator kandydatów / certyfikat / raport sprawdzarki
Obecny stan: kierunek badawczy zgodny z modelem zaufania NPA
Następna walidacja: zmierzony przepływ pracy autora

Zobacz granicę zaufania

Nie znaleziono pasującego obszaru badań.

Spróbuj innego słowa albo wróć filtrem do wszystkich poziomów dojrzałości.

Nano Proof Auditor

Oddziel generowanie dowodów od tego, czemu ufamy.

NPA to łańcuch narzędzi dowodowych, w którym certyfikat jest punktem wyjścia dla dowodów zależnych. Interfejsy, taktyki, wyszukiwanie twierdzeń, wtyczki, AI, pliki źródłowe i status CI mogą pomagać tworzyć kandydatów, ale nie są zaufanym dowodem.

EKSPERYMENTALNEOTWARTY KODAPACHE-2.0

Bieżąca migawka

v0.1.1

Informacje publiczne sprawdzone 2026-06-21.

Główny rdzeń

Rust

Weryfikator i jądro Rust są częścią strony sprawdzania.

Artefakt audytu

.npcert

Kanoniczne bajty certyfikatu są obiektem do inspekcji.

Punkt ponownej kontroli

ręczny przegląd

Stan repozytorium i widoczność pakietu wymagają przeglądu przed publikacją.

Eksplorator granicy zaufania

Przejrzyj, co jest zaufane, a co nie.

Kliknij każdy węzeł, aby zobaczyć, co robi, co produkuje i jakie sprawdzenie jest nadal wymagane.

NIEZAUFANE

SPRAWDZONE

Ważna granica

NPA nie jest obecnie praktycznym zamiennikiem Lean ani Rocq. Ta strona wyjaśnia projektowanie badań skupionych na certyfikatach i nie gwarantuje bezbłędnych systemów komercyjnych ani automatycznego rozwiązywania twierdzeń.

Sprawdzanie certyfikatu / symulacja objaśniająca

Zobacz przepływ sprawdzania certyfikatu.

Interakcja w przeglądarce objaśnia przepływ kontroli. Nie uruchamia NPA, Rust, WASM ani rzeczywistych certyfikatów dowodu.

Przykład CLI

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

NPA / ślad audytu GOTOWE

01 Odczytaj certyfikatkanoniczne bajty / format CZEKAJ
02 Sprawdź hash certyfikatucertificate_hash CZEKAJ
03 Sprawdź w jądrzesprawdzanie dowodu zależnego CZEKAJ
04 Sprawdź ponownie narzędziem referencyjnymwerdykt bez źródeł CZEKAJ
05 Porównaj raport aksjomatówhash raportu aksjomatów CZEKAJ

Werdykt

Objaśnienie nie zostało jeszcze uruchomione.

Uruchom objaśnienie, aby zobaczyć kroki po kolei.

Ekosystem dowodzenia

Wyjaśniaj role zamiast tworzyć ranking narzędzi.

Lean i Rocq to dojrzałe ekosystemy asystentów dowodzenia. NPA pokazujemy tu jako projekt badawczo-implementacyjny skupiony na certyfikatach, a nie ranking zamienników.

Pozycja	Lean	Rocq	NPA
Pozycja	Język programowania o otwartym kodzie i asystent dowodzenia.	Interaktywny system dowodzenia twierdzeń o długiej historii badawczej.	Repozytorium badań i implementacji sprawdzania skupionego na certyfikatach.
Typowe zastosowanie	Matematyka, weryfikacja oprogramowania i programowanie.	Matematyka, specyfikacje, weryfikacja programów i ekstrakcja.	Badania nad certyfikatami dowodu i niezależnym sprawdzaniem.
Wyróżnienie	Rozszerzalność, biblioteki i interaktywne dowodzenie.	Ekspresyjność, dojrzałe metody i biblioteki.	Mała baza zaufania i kanoniczne certyfikaty.
Ujęcie na tej stronie	Punkt odniesienia do nauki, porównań i interoperacyjności.	Punkt odniesienia do nauki, porównań i metod formalizacji.	Projekt badawczy Finite Field.
Granica	Nadal wymagana jest wiedza specjalistyczna.	Nadal wymagana jest wiedza specjalistyczna.	Obecnie nie jest przeznaczony jako praktyczny zamiennik Lean ani Rocq.

Oficjalna strona Lean Oficjalna strona Rocq Prover NPA GitHub

Metoda badawcza

Zamień „zadziałało” w powtarzalną procedurę sprawdzania.

Wynik jest mocniejszy, gdy ktoś może go ponownie uruchomić, skontrolować i odrzucić w tych samych warunkach.

Pytanie

Zdefiniuj, co należy sprawdzić: wydajność, poprawność, zgodność albo zakres.

Założenia

Przed oceną zapisz założenia, wykluczenia, aksjomaty, luki w danych i stronniczość.

Artefakt

Zachowuj źródło, certyfikaty, wejścia, logi wykonania i hashe.

Niezależne sprawdzenie

Sprawdzaj wyniki ścieżką inną niż strona generowania.

Test porównawczy

Ustal sprzęt, wersje, limity czasu, zbiory instancji i ziarna losowe.

Ograniczenia

Publikuj porażki, przypadki nieobsługiwane, granice wydajności i kolejną walidację.

Generator odtwarzalności

Sprawdź, czego nadal brakuje publikacji badawczej.

Lista kontrolna jest przetwarzana tylko w przeglądarce. Nie jest oceną certyfikacyjną.

Gotowość

Pytanie badawcze i warunek sukcesuCo liczy się jako sukces albo porażka. Przypięte narzędzia i zależnościWersje, pliki lock, sprzęt i środowisko. Dane wejściowe lub proces generowaniaAnonimizacja, licencja, źródło i hash. Sekwencja poleceń ponownego uruchomieniaOd inicjalizacji do wygenerowania wyniku. Sprawdzalne artefakty i surowe logiCertyfikaty, raporty, logi i hashe. Ograniczenia, porażki i pytania otwartePrzypadki nieobsługiwane i nierozwiązane kwestie.

Następne działanie

Najpierw zdefiniuj pytanie badawcze i warunek sukcesu.

Przed wyborem formatów artefaktów ustal, co będzie porównywane lub sprawdzane.

Artefakty publiczne

Śledź publiczne artefakty z jednego wejścia.

Strona unika wywołań GitHub API w czasie działania. Stan repozytoriów jest sprawdzoną migawką, którą trzeba zweryfikować przed publikacją.

4 artefakty

finitefield-org

npa

łańcuch narzędzi dowodowych oparty na certyfikatach

Rust / OCamlApache-2.0Eksperymentalne

VERIFY package verify-certs

finitefield-org

npa-std

standardowy pakiet twierdzeń

DowodyPakietEksperymentalne

ROLA Std.Logic / Nat / List

finitefield-org

npa-mathlib

biblioteka matematyki formalnej

MatematykaDowodyBadania

ROLA formalne pakiety twierdzeń

GitHub

finitefield-org

indeks publicznych repozytoriów

OrganizacjaOtwarty kod

INDEKS wszystkie publiczne repozytoria

Żaden publiczny artefakt nie pasuje do wyszukiwania.

Polityka publikacji

Publiczne repozytoria, notatki badawcze i benchmarki powinny zawierać datę sprawdzenia, dojrzałość, kroki odtworzenia i znane ograniczenia. Gwiazdki i liczby commitów nie są pokazywane jako sygnały jakości badań.

Od laboratorium do operacji

Wprowadź dyscyplinę badawczą do projektowania systemów biznesowych.

Nie każdy system klienta potrzebuje dowodzenia twierdzeń. Praktyczna wartość polega na ustaleniu, co ma być zaufane, porównane, sprawdzone, poprawione i zatwierdzone przez ludzi.

Praktyka laboratoryjna

Granice zaufania

Oddziel generowanie, obliczenia i końcowe sprawdzanie zamiast ufać wszystkim warstwom jednakowo.

Dowody

Zachowuj wejścia, wyjścia, certyfikaty, hashe i logi jako artefakty do przeglądu.

Odtwarzalność

Ustal dane, wersje, polecenia i kryteria oceny przed porównaniem wyników.

Ograniczenia

Publikuj ograniczenia, przypadki nieudane i nierozwiązane punkty z taką samą wagą jak wyniki.

System klienta

Uprawnienia i odpowiedzialność

Zdefiniuj, kto wprowadza dane, kto przegląda, kto nadpisuje i kto potwierdza wynik.

Uzasadnienie decyzji

Pokazuj ograniczenia, wyniki oceny, odrzuconych kandydatów i punkty nierozwiązane.

Audytowalność

Zachowuj zmiany warunków, przebiegi obliczeń i historię końcowej akceptacji.

Ocena człowieka

Spraw, aby wynik automatyczny można było poprawić, odrzucić i wyjaśnić operatorom.

01 Planowanie zmian i obsady

Pokazuj naruszenia reguł i spełnienie preferencji oddzielnie.

02 Wyznaczanie tras pojazdów

Utrzymuj widoczne powody tras, pojemność, okna czasowe i wyjątki.

03 Harmonogramowanie produkcji

Wyjaśniaj niezaplanowaną pracę, wąskie gardła i kompromisy ustawień.

04 Dopasowywanie przydziałów

Pokaż powody kandydatów i alternatywy przed zatwierdzeniem.

Notatki badawcze

Zachowuj czytelną historię aktualizacji i dowody.

Nie każda karta jest opublikowanym artykułem. Notatki w przygotowaniu pozostają nieoznaczone jako publikacje, dopóki nie otrzymają dat, źródeł i kroków odtworzenia.

NPA / bieżące2026.06.21

Dlaczego umieszczać certyfikaty w centrum

Dlaczego końcowy dowód powinien być standaryzowanym certyfikatem sprawdzanym małą, niezależną ścieżką.

Zobacz publiczne repozytorium

Notatka projektowa / planowanaW przygotowaniu

Wyjaśnialne wyniki optymalizacji

Notatka projektowa o pokazywaniu celów, twardych ograniczeń, miękkich preferencji i nierozwiązanych przydziałów w UI.

Zobacz powiązane demonstracje

Benchmark / planowanyW przygotowaniu

Warunki uczciwego porównania solverów

Planowana notatka o zestawach instancji, limitach czasu, lukach optymalności, ziarnach losowych i sprzęcie.

Zobacz kryteria publikacji

Pozycje „W przygotowaniu” nie są opublikowanymi artykułami. Po publikacji każda notatka otrzymuje datę, źródło, autora, ścieżkę odtworzenia i znane ograniczenia.

FAQ

Granice badań, narzędzi dowodowych i zastosowań biznesowych.

Te punkty wyjaśniamy, zanim strony badawcze zostaną pomylone z gwarancjami produkcyjnymi.

Poznaj firmę

01 Czy Laboratorium matematyczne jest usługą kontraktowego rozwoju?

Nie. To miejsce publikowania podejścia badawczego i artefaktów. W rozmowach z klientami oddzielamy metody możliwe do zastosowania, metody wymagające dalszej walidacji i tematy badawcze.

02 Czy NPA może zastąpić Lean lub Rocq?

Nie. Obecne NPA nie jest praktycznym zamiennikiem Lean ani Rocq. To projekt badawczo-implementacyjny dotyczący certyfikatów, niezależnego sprawdzania i małej bazy zaufania.

03 Czy ufasz dowodom wygenerowanym przez AI bez zmian?

Nie. AI, wyszukiwanie i taktyki pomagają generować kandydatów. Skupiamy się na tym, czy końcowy certyfikat akceptuje sprawdzarka niezależna od tych ścieżek generowania.

04 Czy weryfikacja formalna usuwa wszystkie błędy?

Nie. Metody formalne sprawdzają konkretne własności względem jawnej specyfikacji. Błędne specyfikacje, kod poza zakresem, operacje i usługi zewnętrzne nadal wymagają osobnego przeglądu.

05 Czy to wiąże się z pracą nad systemami biznesowymi?

Tak. Zwykle stosujemy tę dyscyplinę stopniowo: ograniczenia, powody wyników, historię obliczeń, granice uprawnień i kontrole ważnej logiki biznesowej.

Omów problem

Możesz omówić pracę do rozwiązania, nie tylko temat badawczy.

Zacznij od obecnego arkusza, reguł i miejsc, w których ludzie poprawiają decyzje. Możemy ustalić, czy najpierw potrzebne jest modelowanie matematyczne, automatyzacja reguł czy prototyp.

Sprawdź problem biznesowy Zobacz prototyp

Migawka źródeł / 2026-06-21

Twierdzenia dotyczące NPA opierają się na migawce repozytorium finitefield-org/npa. Pozycjonowanie Lean i Rocq opiera się na ich oficjalnych stronach. Stan repozytorium, najnowsze tagi i sformułowania dotyczące przeglądu metody sprawdzono 2026-06-28.