Finite Field / Matematické laboratórium

Budujte dôkazy správnosti, nielen rýchle výsledky.

Matematické laboratórium ukazuje, ako pracujeme s matematickým modelovaním, dokazovaním viet, formálnym overovaním, reprodukovateľnosťou a dôveryhodnou implementáciou bez nadhodnocovania dôkazov.

Zobraziť výskumné oblasti Otvoriť stránku NPA

Verejné projekty: NPA / STD / MATHLIB
Hlavný jazyk: Rust
Snímka NPA: v0.1.1

Audit dôkazov / koncepčný pohľad Len na čítanie

01 kanonické bajty / formát OK

02 certificate_hash OK

03 kontrola závislého dôkazu OK

04 verdikt bez zdrojov OK

Viditeľná hranica dôvery Táto stránka netvrdí, že NPA je praktická náhrada za Lean alebo Rocq, a simulácia v prehliadači NPA nespúšťa.

Princíp laboratória

Publikujte nielen výsledky, ale aj hranicu kontroly.

Záver typu „fungovalo to“, „bolo to rýchle“ alebo „bolo to dokázané“ nestačí. Samostatne ukazujeme vstupy, predpoklady, dôveryhodné časti, nezávisle kontrolovateľné artefakty a nevyriešené otázky.

01 / Hranica

Udržujte dôveryhodné jadro malé

Neumiestňujte zložité generátory ani AI do stredu dôvery. Malú kontrolnú stranu urobte výslovnou.

02 / Dôkazy

Urobte z dôkazov artefakt

Certifikáty, hashe, zoznamy predpokladov, podmienky porovnávacích testov a logy nechajte v podobe, ktorú môžu ostatní skontrolovať.

03 / Reprodukcia

Navrhujte pre reprodukovateľnosť

Pripnite nástrojové reťazce, vstupné údaje, príkazy spustenia a kritériá, aby sa výsledok dal skontrolovať znova.

04 / Poctivosť

Nepreceňujte stav výskumu

Praktické metódy, experimenty a výskum ukazujte oddelene. Obmedzenia dávajte vedľa výsledkov.

KONTROLA METÓDY

Kategória servisnej metódy, ktorá pred označením za pripravenú na projekt stále vyžaduje rozsah, zodpovednosť, klientské dôkazy a schválenie.

EXPERIMENTÁLNE

Funkčná implementácia existuje, ale rozsah, kompatibilita, výkon alebo špecifikácia sa môžu meniť. Vyžadujú sa verzia a reprodukčné kroky.

VÝSKUM

Návrh, hodnotenie, dôkaz alebo implementácia prebieha. Neznamená to komerčnú dostupnosť ani dokončenie.

Výskumné portfólio

Zobrazte výskum podľa zrelosti a artefaktov.

Každá karta ukazuje zrelosť, artefakty, aktuálny stav a ďalšie overenie. Vyhľadávanie a filtre používajú iba stav v prehliadači.

8 zobrazené

EXPERIMENTÁLNE OTVORENÝ ZDROJ

Nano Proof Auditor

Dôkazový nástrojový reťazec s certifikátom na prvom mieste

Výskumný nástrojový reťazec, ktorý kladie kanonické dôkazové certifikáty a malú kontrolnú základňu do stredu kontroly závislých dôkazov.

Artefakty: zdroj / špecifikácia / šablóny CI
Aktuálne: verejná snímka v0.1.1
Ďalšie overenie: externé balíky viet a nezávislá kontrola

Otvoriť detail NPA

EXPERIMENTÁLNE OTVORENÝ ZDROJ

NPA Standard Library

Logic / Nat / List / Algebra

Repozitár štandardných balíkov viet pre opakovane použiteľné základy NPA.

Artefakty: zdroj / dôkazové balíky
Aktuálne: verejný oddelený repozitár
Ďalšie overenie: rozsah balíka a kompatibilita

GitHub

VÝSKUM OTVORENÝ ZDROJ

NPA Math Library

Knižnica formálnej matematiky

Smer knižnice na ukladanie matematických viet ako nezávisle kontrolovateľných dôkazových balíkov.

Artefakty: zdroj / dôkazové balíky
Aktuálne: verejný repozitár vo vývoji
Ďalšie overenie: štruktúra knižnice a audit závislostí

GitHub

KONTROLA METÓDY METÓDA

Modely plánovania s obmedzeniami

Smeny / Trasy / Priraďovanie

Metóda na oddeľovanie pevných obmedzení a hodnotiacich metrík pri smenách, návštevách, trasách, výrobe a priraďovaní.

Artefakty: model / prototyp / vysvetľujúca správa
Aktuálne: štúdia rozsahu a dôkazov
Ďalšie overenie: klientské dôkazy a schválenie rozsahu

Zobraziť prototyp

VÝSKUM MERANIE

Reprodukovateľné hodnotenie riešičov

Benchmark a dôkazy

Program na fixovanie množín inštancií, hardvéru, časových limitov, náhodných semien a surových logov pred tvrdeniami o výkone.

Artefakty: register porovnávacích testov / surové logy / správa
Aktuálne: návrh výskumného programu
Ďalšie overenie: prvý verejný korpus benchmarkov

Zobraziť metódu

VÝSKUM FORMÁLNE METÓDY

Overovanie kritickej obchodnej logiky

Invarianty pre podnikové systémy

Výskum oddeľovania poplatkov, oprávnení, zásob a stavových prechodov do špecifikácií a invariantov.

Artefakty: špecifikácia / invarianty / test alebo dôkazová správa
Aktuálne: štúdia rozsahu
Ďalšie overenie: vybrať jeden ohraničený prípad podobný produkcii

Zobraziť návrh bezpečnosti

EXPERIMENTÁLNE INŽINIERSTVO

Malé dôveryhodné komponenty v Ruste

Malé dôveryhodné časti

Implementačná práca, ktorá drží časti kritické pre dôveru, ako kontrolóry a hashe, dosť malé na kontrolu.

Artefakty: jadro NPA / crate certifikátu / referenčný kontrolór
Aktuálne: verejná implementácia v NPA
Ďalšie overenie: kompatibilita nezávislého kontrolóra

Zobraziť zdroj

VÝSKUM AI × DÔKAZ

Pomoc AI a nezávislá kontrola

Generovať voľne, overovať prísne

Výskumný smer, ktorý ponecháva AI pri generovaní kandidátov, zatiaľ čo konečný dôkaz sa kontroluje nezávisle.

Artefakty: generátor kandidátov / certifikát / správa kontrolóra
Aktuálne: výskumný smer v súlade s modelom dôvery NPA
Ďalšie overenie: meraný autorský pracovný tok

Zobraziť hranicu dôvery

Nenašla sa zodpovedajúca výskumná oblasť.

Skúste iné kľúčové slovo alebo vráťte filter zrelosti na všetko.

Nano Proof Auditor

Oddeľte generovanie dôkazov od toho, čomu dôverujeme.

NPA je dôkazový nástrojový reťazec so zameraním na certifikáty pre závislé dôkazy. Rozhrania, taktiky, vyhľadávanie viet, pluginy, AI, zdrojové súbory a stav CI môžu pomáhať vytvárať kandidátov, ale nie sú dôveryhodným dôkazom.

EXPERIMENTÁLNEOPEN SOURCEAPACHE-2.0

Aktuálna snímka

v0.1.1

Verejné informácie skontrolované 2026-06-21.

Primárne jadro

Rust

Rust overovač a jadro sú súčasťou kontrolnej strany.

Auditný artefakt

.npcert

Kanonické bajty certifikátu sú objektom na kontrolu.

Bod opätovnej kontroly

ručná kontrola

Stav repozitára a viditeľnosť balíkov treba pred publikovaním preskúmať.

Prieskumník hranice dôvery

Preklikajte si, čomu sa dôveruje a čomu nie.

Kliknite na každý uzol a pozrite si, čo robí, čo produkuje a aká kontrola je stále potrebná.

NEDÔVERYHODNÉ

SKONTROLOVANÉ

Dôležitá hranica

NPA v súčasnosti nie je praktickou náhradou za Lean alebo Rocq. Táto stránka vysvetľuje výskumný návrh sústredený na certifikáty a nezaručuje bezchybné komerčné systémy ani automatické dokazovanie viet.

Kontrola certifikátu / vysvetľujúca simulácia

Vyskúšajte tok kontroly certifikátu.

Interakcia v prehliadači vysvetľuje tok kontroly. Nespúšťa NPA, Rust, WASM ani skutočné dôkazové certifikáty.

Príklad CLI

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

NPA / audit trace PRIPRAVENÉ

01 Prečítať certifikátkanonické bajty / formát ČAKÁ
02 Skontrolovať hash certifikátucertificate_hash ČAKÁ
03 Skontrolovať jadromkontrola závislého dôkazu ČAKÁ
04 Opätovne skontrolovať referenčným kontrolóromverdikt bez zdrojov ČAKÁ
05 Porovnať správu o axiómachhash správy o axiómach ČAKÁ

Verdikt

Vysvetlenie ešte nebolo spustené.

Spustite vysvetlenie a zobrazte kroky v poradí.

Ekosystém dôkazov

Ujasnite roly namiesto rebríčka nástrojov.

Lean a Rocq sú zrelé ekosystémy dokazovacích asistentov. NPA tu ukazujeme ako výskumný a implementačný projekt zameraný na certifikáty, nie ako náhradný rebríček.

Položka	Lean	Rocq	NPA
Pozícia	Open-source programovací jazyk a dokazovací asistent.	Interaktívny dokazovač viet s dlhou výskumnou históriou.	Výskumný a implementačný repozitár pre kontrolu s certifikátmi na prvom mieste.
Typické použitie	Matematika, overovanie softvéru a programovanie.	Matematika, špecifikácie, overovanie programov a extrakcia.	Výskum dôkazových certifikátov a nezávislej kontroly.
Dôraz	Rozšíriteľnosť, knižnice a interaktívne dokazovanie.	Vyjadrovacia sila, zrelé metódy a knižnice.	Malá dôveryhodná základňa a kanonické certifikáty.
Ako s tým pracuje táto stránka	Referencia pre učenie, porovnanie a interoperabilitu.	Referencia pre učenie, porovnanie a metódy formalizácie.	Výskumný projekt Finite Field.
Hranica	Špecializované znalosti sú stále potrebné.	Špecializované znalosti sú stále potrebné.	V tejto chvíli nie je určené ako praktická náhrada za Lean alebo Rocq.

Oficiálna stránka Lean Oficiálna stránka Rocq Prover NPA GitHub

Výskumná metóda

Zmeňte „fungovalo to“ na opakovateľný kontrolný postup.

Výsledok je silnejší, keď ho niekto môže za rovnakých podmienok znovu spustiť, preskúmať a odmietnuť.

Otázka

Definujte, čo sa má kontrolovať: výkon, správnosť, kompatibilita alebo rozsah.

Predpoklady

Pred hodnotením zapíšte predpoklady, vylúčenia, axiómy, medzery v údajoch a skreslenie.

Artefakt

Uchovajte zdroj, certifikáty, vstupy, logy spustenia a hashe.

Nezávislá kontrola

Výsledky kontrolujte cestou odlišnou od generujúcej strany.

Benchmark

Fixujte hardvér, verzie, časové limity, množiny inštancií a náhodné semená.

Limity

Publikujte zlyhania, nepodporované prípady, hranice výkonu a ďalšie overenie.

Tvorca reprodukovateľnosti

Skontrolujte, čo výskumnej publikácii ešte chýba.

Kontrolný zoznam sa spracúva iba v prehliadači. Nie je to certifikačné skóre.

Pripravenosť

Výskumná otázka a podmienka úspechuČo sa počíta ako úspech alebo zlyhanie. Pripnuté nástroje a závislostiVerzie, lock súbory, hardvér a prostredie. Vstupné údaje alebo proces generovaniaAnonymizácia, licencia, zdroj a hash. Postupnosť príkazov na opätovné spustenieOd inicializácie po vytvorenie výsledku. Kontrolovateľné artefakty a surové logyCertifikáty, správy, logy a hashe. Limity, zlyhania a otvorené otázkyNepodporované prípady a nevyriešené otázky.

Ďalšia akcia

Najprv definujte výskumnú otázku a podmienku úspechu.

Pred rozhodnutím o formátoch artefaktov fixujte, čo sa bude porovnávať alebo kontrolovať.

Verejné artefakty

Sledujte verejné artefakty z jedného vstupu.

Stránka sa vyhýba volaniam GitHub API počas behu. Stav repozitárov je skontrolovaná snímka, ktorú treba pred publikovaním overiť.

4 artefaktov

finitefield-org

npa

dôkazový nástrojový reťazec s certifikátom na prvom mieste

Rust / OCamlApache-2.0Experimentálne

OVERIŤ package verify-certs

finitefield-org

npa-std

štandardný balík viet

DôkazyBalíkExperimentálne

ROLA Std.Logic / Nat / List

finitefield-org

npa-mathlib

knižnica formálnej matematiky

MatematikaDôkazyVýskum

ROLA formálne balíky viet

GitHub

finitefield-org

index verejných repozitárov

OrganizáciaOtvorený zdroj

INDEX všetky verejné repozitáre

Žiadny verejný artefakt nezodpovedá vyhľadávaniu.

Politika publikovania

Verejné repozitáre, výskumné poznámky a porovnávacie testy majú niesť dátum kontroly, zrelosť, reprodukčné kroky a známe obmedzenia. Hviezdičky a počty commitov sa neukazujú ako signály kvality výskumu.

Z laboratória do prevádzky

Preneste výskumnú disciplínu do návrhu podnikových systémov.

Nie každý klientsky systém potrebuje dokazovanie viet. Užitočný prenos spočíva v rozhodnutí, čomu treba dôverovať, čo porovnávať, kontrolovať, opravovať a čo majú ľudia schvaľovať.

Laboratórna prax

Hranice dôvery

Oddeľte generovanie, výpočet a konečnú kontrolu namiesto toho, aby ste všetkým vrstvám dôverovali rovnako.

Dôkazy

Vstupy, výstupy, certifikáty, hashe a logy uchovajte ako kontrolovateľné artefakty.

Reprodukovateľnosť

Pred porovnávaním výsledkov pripnite údaje, verzie, príkazy a hodnotiace kritériá.

Limity

Obmedzenia, zlyhané prípady a nevyriešené body publikujte s rovnakou váhou ako výsledky.

Klientsky systém

Právomoc a zodpovednosť

Definujte, kto zadáva vstupy, kto kontroluje, kto prepisuje a kto potvrdzuje výsledok.

Dôvody rozhodnutia

Ukazujte obmedzenia, hodnotiace skóre, odmietnutých kandidátov a nevyriešené body.

Auditovateľnosť

Zachovajte zmeny podmienok, behy výpočtov a históriu konečného schválenia.

Ľudský úsudok

Automatizovaný výstup musí byť pre operátorov opraviteľný, odmietnuteľný a vysvetliteľný.

01 Smeny a obsadenie

Porušenia pravidiel a splnenie preferencií zobrazujte oddelene.

02 Trasy vozidiel

Dôvody trás, kapacitu, časové okná a výnimky nechajte viditeľné.

03 Plánovanie výroby

Vysvetlite nenaplánovanú prácu, úzke miesta a kompromisy nastavenia.

04 Priraďovanie úloh

Pred schválením zobrazte dôvody kandidátov a alternatívy.

Výskumné poznámky

Udržujte históriu aktualizácií a dôkazy čitateľné.

Nie každá karta je publikovaný článok. Prípravné poznámky zostávajú neoznačené ako publikovaná práca, kým nezískajú dátumy, zdroje a reprodukčné kroky.

NPA / Aktuálne2026.06.21

Prečo dať certifikáty do stredu

Prečo má byť konečným dôkazom štandardizovaný certifikát kontrolovaný malou nezávislou cestou.

Zobraziť verejný repozitár

Návrhová poznámka / plánovanéPripravuje sa

Ako urobiť výsledky optimalizácie vysvetliteľné

Návrhová poznámka o zobrazovaní cieľov, pevných obmedzení, mäkkých preferencií a nevyriešených priradení v rozhraní.

Zobraziť súvisiace ukážky

Benchmark / plánovanéPripravuje sa

Podmienky férového porovnania riešičov

Plánovaná poznámka o množinách inštancií, časových limitoch, medzerách optimality, náhodných semenách a hardvéri.

Zobraziť kritériá publikovania

Položky „v príprave“ nie sú publikované články. Po publikovaní každá poznámka dostane dátum, zdroj, autora, reprodukčnú cestu a známe obmedzenia.

Časté otázky

Hranice výskumu, dôkazových nástrojov a obchodného použitia.

Tieto body výslovne uvádzame skôr, než sa výskumné stránky omylom považujú za produkčné záruky.

Prečítať o spoločnosti

01 Je Matematické laboratórium služba zmluvného vývoja?

Nie. Je to miesto na publikovanie výskumného postoja a artefaktov. Pri rozhovoroch s klientmi oddeľujeme použiteľné metódy, metódy vyžadujúce ďalšie overenie a výskumné témy.

02 Môže NPA nahradiť Lean alebo Rocq?

Nie. Súčasné NPA nie je praktickou náhradou za Lean alebo Rocq. Je to výskumný a implementačný projekt okolo certifikátov, nezávislej kontroly a malej dôveryhodnej základne.

03 Dôverujete dôkazom vygenerovaným AI tak, ako sú?

Nie. AI, vyhľadávanie a taktiky pomáhajú generovať kandidátov. Zameriavame sa na to, či konečný certifikát prijme kontrolór nezávislý od týchto generujúcich ciest.

04 Odstráni formálne overovanie všetky chyby?

Nie. Formálne metódy kontrolujú konkrétne vlastnosti voči výslovnej špecifikácii. Nesprávne špecifikácie, kód mimo rozsahu, prevádzka a externé služby stále vyžadujú samostatnú kontrolu.

05 Súvisí to s prácou na podnikových systémoch?

Áno. Disciplínu zvyčajne uplatňujeme postupne: obmedzenia, dôvody výsledkov, história výpočtov, hranice oprávnení a kontroly dôležitej obchodnej logiky.

Prediskutovať problém

Môžete prediskutovať prácu, ktorú treba vyriešiť, nielen výskumnú tému.

Začnite od aktuálnej tabuľky, pravidiel a miest, kde ľudia opravujú rozhodnutia. Pomôžeme roztriediť, či má byť prvým krokom matematické modelovanie, automatizácia pravidiel alebo prototyp.

Skontrolovať obchodný problém Zobraziť prototyp

Snímka zdrojov / 2026-06-21

Tvrdenia o NPA vychádzajú zo snímky repozitára finitefield-org/npa. Pozícia Lean a Rocq vychádza z ich oficiálnych stránok. Stav repozitára, najnovšie tagy a formulácie kontroly metódy boli skontrolované 2026-06-28.