Finite Field / Math Lab

Budujte důkazní podklady správnosti, nejen rychlé výsledky.

Math Lab ukazuje, jak pracujeme s matematickým modelováním, dokazováním vět, formálním ověřováním, reprodukovatelností a důvěryhodnou implementací, aniž bychom přeháněli sílu důkazů.

Zobrazit oblasti výzkumu Otevřít stránku NPA

Veřejné projekty: NPA / STD / MATHLIB
Hlavní jazyk: Rust
Snímek NPA: v0.1.1

Audit důkazů / koncepční pohled Jen pro čtení

01 kanonické bajty / formát OK

02 certificate_hash OK

03 kontrola závislých důkazů OK

04 verdikt bez zdrojového kódu OK

Viditelná hranice důvěry Tato stránka netvrdí, že NPA je praktická náhrada za Lean nebo Rocq, a simulace v prohlížeči NPA nespouští.

Princip laboratoře

Zveřejňujte nejen výsledky, ale i hranici kontroly.

Závěr typu „fungovalo to“, „bylo to rychlé“ nebo „bylo to dokázáno“ nestačí. Samostatně ukazujeme vstupy, předpoklady, důvěryhodné části, nezávisle ověřitelné artefakty a nevyřešené otázky.

01 / Hranice

Udržujte důvěryhodnou základnu malou

Nestavte složité generátory ani AI do středu důvěry. Malou kontrolní stranu popište výslovně.

02 / Důkazy

Udělejte z důkazů artefakt

Certifikáty, hashe, seznamy předpokladů, podmínky benchmarků a logy ponechte ve formě, kterou mohou ostatní zkontrolovat.

03 / Reprodukce

Navrhujte pro reprodukovatelnost

Pevně stanovte toolchainy, vstupní data, příkazy spuštění a kritéria, aby šel výsledek znovu ověřit.

04 / Poctivost

Nepřeceňujte stav výzkumu

Praktické metody, experimenty a výzkum ukazujte odděleně. Omezení uvádějte vedle výsledků.

REVIZE METODY

Kategorie servisní metody, která před označením za připravenou pro projekt stále vyžaduje rozsah, odpovědnost, klientské podklady a schválení.

EXPERIMENTÁLNÍ

Funkční implementace existuje, ale stále se mohou měnit měřítko, kompatibilita, výkon nebo specifikace. Je nutné uvést verzi a kroky reprodukce.

VÝZKUM

Návrh, hodnocení, důkaz nebo implementace stále probíhá. Neznamená to komerční dostupnost ani dokončení.

Výzkumné portfolio

Prohlížejte výzkum podle zralosti a artefaktů.

Každá karta ukazuje zralost, artefakty, aktuální stav a další ověření. Vyhledávání a filtry používají pouze stav v prohlížeči.

8 zobrazeno

EXPERIMENTÁLNÍ OPEN SOURCE

Nano Proof Auditor

Důkazní toolchain založený nejdříve na certifikátech

Výzkumný toolchain, který staví kanonické důkazní certifikáty a malou kontrolní základnu do středu revize závislých důkazů.

Artefakty: zdroj / specifikace / šablony CI
Aktuálně: veřejný snímek v0.1.1
Další ověření: externí balíčky vět a nezávislá kontrola

Otevřít detail NPA

EXPERIMENTÁLNÍ OPEN SOURCE

Standardní knihovna NPA

Logika / přirozená čísla / seznamy / algebra

Repozitář standardních balíčků vět pro znovupoužitelné základy NPA.

Artefakty: zdroj / důkazní balíčky
Aktuálně: veřejný oddělený repozitář
Další ověření: rozsah balíčku a kompatibilita

GitHub

VÝZKUM OPEN SOURCE

Matematická knihovna NPA

Knihovna formální matematiky

Směr knihovny pro ukládání matematických vět jako nezávisle kontrolovatelných důkazních balíčků.

Artefakty: zdroj / důkazní balíčky
Aktuálně: veřejný repozitář ve vývoji
Další ověření: struktura knihovny a audit závislostí

GitHub

REVIZE METODY METODA

Modely plánování s omezeními

Plánování / trasy / přiřazení

Metoda pro oddělení tvrdých omezení a hodnoticích metrik u směn, návštěv, tras, výroby a přiřazování.

Artefakty: model / prototyp / vysvětlující zpráva
Aktuálně: servisní metoda; veřejné tvrzení omezené na revizi metody
Další ověření: klientské podklady a schválení rozsahu

Zobrazit prototyp

VÝZKUM MĚŘENÍ

Reprodukovatelné hodnocení řešičů

Benchmark a důkazní podklady

Program pro pevné stanovení sad instancí, hardwaru, časových limitů, náhodných semen a surových logů před tvrzeními o výkonu.

Artefakty: registr benchmarků / surové logy / zpráva
Aktuálně: návrh výzkumného programu
Další ověření: první veřejný korpus benchmarků

Zobrazit metodu

VÝZKUM FORMÁLNÍ METODY

Ověřování kritické provozní logiky

Invarianty pro provozní systémy

Výzkum převodu poplatků, oprávnění, zásob a stavových přechodů do specifikací a invariantů.

Artefakty: specifikace / invarianty / testovací nebo důkazní zpráva
Aktuálně: studie rozsahu
Další ověření: vybrat jeden omezený případ podobný produkci

Zobrazit návrh zabezpečení

EXPERIMENTÁLNÍ INŽENÝRSTVÍ

Malé důvěryhodné komponenty v Rustu

Malé důvěryhodné komponenty

Implementační práce, která udržuje důvěrově kritické části, například ověřovače a hashe, dostatečně malé pro kontrolu.

Artefakty: jádro NPA / crate certifikátů / referenční ověřovač
Aktuálně: veřejná implementace v NPA
Další ověření: kompatibilita nezávislého ověřovače

Zobrazit zdroj

VÝZKUM AI × DŮKAZ

Pomoc AI a nezávislá kontrola

Generovat volně, ověřovat přísně

Výzkumný směr, který ponechává AI při generování kandidátů, zatímco konečný důkazní podklad je ověřen nezávisle.

Artefakty: generátor kandidátů / certifikát / zpráva ověřovače
Aktuálně: výzkumný směr v souladu s modelem důvěry NPA
Další ověření: měřený autorský postup

Zobrazit hranici důvěry

Nebyla nalezena žádná odpovídající oblast výzkumu.

Zkuste jiné klíčové slovo nebo vraťte filtr zralosti na všechny položky.

Nano Proof Auditor

Oddělte generování důkazů od toho, čemu důvěřujeme.

NPA je důkazní toolchain pro závislé důkazy, který staví certifikáty na první místo. Front-endy, taktiky, vyhledávání vět, pluginy, AI, zdrojové soubory a stav CI mohou pomoci vytvořit kandidáty, ale nejsou důvěryhodným důkazním podkladem.

EXPERIMENTÁLNÍOPEN SOURCEAPACHE-2.0

Aktuální snímek

v0.1.1

Veřejné informace zkontrolovány 2026-06-21.

Primární jádro

Rust

Ověřovač v Rustu a jádro jsou součástí kontrolní strany.

Auditní artefakt

.npcert

Kanonické bajty certifikátu jsou objektem kontroly.

Bod opětovné kontroly

ruční kontrola

Před zveřejněním je nutné zkontrolovat stav repozitáře a viditelnost balíčku.

Průzkumník hranice důvěry

Projděte si, čemu se důvěřuje a čemu ne.

Kliknutím na každý uzel zjistíte, co dělá, co vytváří a jaká kontrola je stále potřeba.

UNTRUSTED

CHECKED

Důležitá hranice

NPA v současnosti není praktickou náhradou za Lean nebo Rocq. Tato stránka vysvětluje výzkumný návrh zaměřený na certifikáty a nezaručuje bezchybné komerční systémy ani automatické řešení vět.

Kontrola certifikátu / vysvětlující simulace

Projděte si tok kontroly certifikátu.

Interakce v prohlížeči vysvětluje tok kontroly. Nespouští NPA, Rust, WASM ani skutečné důkazní certifikáty.

Příklad CLI

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

NPA / auditní stopa PŘIPRAVENO

01 Přečíst certifikátkanonické bajty / formát ČEKÁ
02 Zkontrolovat hash certifikátucertificate_hash ČEKÁ
03 Zkontrolovat jádremkontrola závislých důkazů ČEKÁ
04 Znovu zkontrolovat referenčním ověřovačemverdikt bez zdrojového kódu ČEKÁ
05 Porovnat zprávu o axiomechhash zprávy o axiomech ČEKÁ

Verdikt

Vysvětlení ještě nebylo spuštěno.

Spusťte vysvětlení, aby se kroky zobrazily v pořadí.

Ekosystém důkazů

Vyjasněte role místo řazení nástrojů.

Lean a Rocq jsou vyspělé ekosystémy pro asistované dokazování. NPA je zde uveden jako výzkumný a implementační projekt zaměřený na certifikáty, ne jako žebříček náhrad.

Položka	Lean	Rocq	NPA
Postavení	Open-source programovací jazyk a asistent pro dokazování.	Interaktivní dokazovač vět s dlouhou výzkumnou historií.	Výzkumný a implementační repozitář pro kontrolu založenou nejdříve na certifikátech.
Typické použití	Matematika, ověřování softwaru a programování.	Matematika, specifikace, ověřování programů a extrakce.	Výzkum důkazních certifikátů a nezávislé kontroly.
Důraz	Rozšiřitelnost, knihovny a interaktivní dokazování.	Vyjadřovací síla, vyspělé metody a knihovny.	Malá důvěryhodná základna a kanonické certifikáty.
Jak s tím tato stránka pracuje	Reference pro učení, porovnání a interoperabilitu.	Reference pro učení, porovnání a formalizační metody.	Výzkumný projekt Finite Field.
Hranice	Stále jsou potřeba odborné znalosti.	Stále jsou potřeba odborné znalosti.	V tuto chvíli není zamýšlen jako praktická náhrada za Lean nebo Rocq.

Oficiální web Lean Oficiální web Rocq Prover NPA na GitHubu

Výzkumná metoda

Proměňte „fungovalo to“ v opakovatelný kontrolní postup.

Výsledek je silnější, když ho někdo může za stejných podmínek znovu spustit, zkontrolovat a případně odmítnout.

Otázka

Určete, co se má kontrolovat: výkon, správnost, kompatibilita nebo rozsah.

Předpoklady

Před hodnocením sepište předpoklady, výluky, axiomy, mezery v datech a možná zkreslení.

Artefakt

Uchovávejte zdroj, certifikáty, vstupy, logy spuštění a hashe.

Nezávislá kontrola

Výsledky kontrolujte cestou odlišnou od strany generování.

Benchmark

Pevně stanovte hardware, verze, časové limity, sady instancí a náhodná semena.

Limity

Zveřejněte selhání, nepodporované případy, hranice výkonu a další ověření.

Průvodce reprodukovatelností

Zkontrolujte, co výzkumné publikaci ještě chybí.

Kontrolní seznam se zpracovává pouze v prohlížeči. Není to certifikační skóre.

Připravenost

Výzkumná otázka a podmínka úspěchuCo se počítá jako úspěch nebo selhání. Pevně stanovené nástroje a závislostiVerze, lock soubory, hardware a prostředí. Vstupní data nebo proces generováníAnonymizace, licence, zdroj a hash. Sekvence příkazů pro opakované spuštěníOd inicializace po vygenerování výsledku. Kontrolovatelné artefakty a surové logyCertifikáty, zprávy, logy a hashe. Limity, selhání a otevřené otázkyNepodporované případy a nevyřešené otázky.

Další akce

Nejdřív definujte výzkumnou otázku a podmínku úspěchu.

Než určíte formáty artefaktů, ujasněte, co se bude porovnávat nebo kontrolovat.

Veřejné artefakty

Sledujte veřejné artefakty z jednoho vstupu.

Stránka se vyhýbá runtime voláním GitHub API. Stav repozitářů je zkontrolovaný snímek, který je nutné před zveřejněním znovu prověřit.

4 artefakty

finitefield-org

npa

důkazní toolchain založený nejdříve na certifikátech

Rust / OCamlApache-2.0Experimentální

OVĚŘIT package verify-certs

finitefield-org

npa-std

standardní balíček vět

DůkazyBalíčekExperimentální

ROLE Std.Logic / Nat / List

finitefield-org

npa-mathlib

knihovna formální matematiky

MatematikaDůkazyVýzkum

ROLE formální balíčky vět

GitHub

finitefield-org

index veřejných repozitářů

OrganizaceOpen source

INDEX všechny veřejné repozitáře

Vyhledávání neodpovídá žádný veřejný artefakt.

Zásady zveřejnění

Veřejné repozitáře, výzkumné poznámky a benchmarky mají uvádět datum kontroly, zralost, kroky reprodukce a známá omezení. Počty hvězd ani commitů se neuvádějí jako signály kvality výzkumu.

Od laboratoře k provozu

Přeneste výzkumnou disciplínu do návrhu provozních systémů.

Ne každý klientský systém potřebuje dokazování vět. Užitečný přenos spočívá v určení, čemu se má věřit, co porovnat, zkontrolovat, opravit a schválit lidmi.

Praxe z laboratoře

Hranice důvěry

Oddělte generování, výpočet a konečnou kontrolu, místo aby se všem vrstvám věřilo stejně.

Důkazní podklady

Uchovávejte vstupy, výstupy, certifikáty, hashe a logy jako kontrolovatelné artefakty.

Reprodukovatelnost

Před porovnáním výsledků pevně stanovte data, verze, příkazy a hodnoticí kritéria.

Limity

Zveřejňujte omezení, neúspěšné případy a nevyřešené body se stejnou váhou jako výsledky.

Klientský systém

Pravomoc a odpovědnost

Určete, kdo zadává vstupy, kdo kontroluje, kdo provádí změny a kdo výsledek potvrzuje.

Důvody rozhodnutí

Zobrazujte omezení, hodnoticí skóre, odmítnuté kandidáty a nevyřešené body.

Auditovatelnost

Uchovávejte změny podmínek, běhy výpočtů a historii konečného schválení.

Lidský úsudek

Automatický výstup musí být pro operátory opravitelný, odmítnutelný a vysvětlitelný.

01 Směny a obsazení

Porušení pravidel a splnění preferencí zobrazujte odděleně.

02 Plánování tras vozidel

Důvody trasy, kapacitu, časová okna a výjimky ponechte viditelné.

03 Plánování výroby

Vysvětlete nenaplánovanou práci, úzká místa a kompromisy při seřízení.

04 Párování přiřazení

Před schválením zobrazte důvody kandidátů a alternativy.

Výzkumné poznámky

Udržujte historii změn a důkazní podklady čitelné.

Ne každá karta je zveřejněný článek. Přípravné poznámky nejsou označeny jako publikovaná práce, dokud nemají datum, zdroje a kroky reprodukce.

NPA / Current2026.06.21

Proč postavit certifikáty do středu

Proč by konečným důkazním podkladem měl být standardizovaný certifikát ověřený malou nezávislou cestou.

Zobrazit veřejný repozitář

Design note / plannedPřipravuje se

Jak zajistit vysvětlitelnost výsledků optimalizace

Návrhová poznámka o zobrazení cílů, tvrdých omezení, měkkých preferencí a nevyřešených přiřazení v UI.

Zobrazit související ukázky

Benchmark / plannedPřipravuje se

Podmínky pro férové porovnání řešičů

Plánovaná poznámka o sadách instancí, časových limitech, mezerách optimality, náhodných semenech a hardwaru.

Zobrazit kritéria zveřejnění

Položky „Připravuje se“ nejsou zveřejněné články. Po zveřejnění každá poznámka dostane datum, zdroj, autora, reprodukční postup a známá omezení.

FAQ

Hranice výzkumu, důkazních nástrojů a využití v provozu.

Tyto body uvádíme výslovně, aby se výzkumné stránky nezaměňovaly za produkční záruky.

Přečíst si o společnosti

01 Je Math Lab služba smluvního vývoje?

Ne. Je to místo pro zveřejnění výzkumného přístupu a artefaktů. V klientských diskusích oddělujeme použitelné metody, metody vyžadující další ověření a témata ve fázi výzkumu.

02 Může NPA nahradit Lean nebo Rocq?

Ne. Současné NPA není praktická náhrada za Lean nebo Rocq. Jde o výzkumný a implementační projekt kolem certifikátů, nezávislé kontroly a malé důvěryhodné základny.

03 Důvěřujete důkazům vygenerovaným AI tak, jak jsou?

Ne. AI, vyhledávání a taktiky pomáhají generovat kandidáty. Zaměřujeme se na to, zda konečný certifikát přijme ověřovač nezávislý na těchto cestách generování.

04 Odstraní formální ověření všechny chyby?

Ne. Formální metody ověřují konkrétní vlastnosti vůči výslovné specifikaci. Chybné specifikace, kód mimo rozsah, provozní postupy a externí služby stále vyžadují samostatnou kontrolu.

05 Souvisí to s prací na provozních systémech?

Ano. Tuto disciplínu obvykle uplatňujeme postupně: omezení, důvody výsledků, historii výpočtů, hranice oprávnění a kontroly důležité provozní logiky.

Probrat problém

Můžete probrat práci, kterou je třeba vyřešit, ne jen samotné výzkumné téma.

Začněte aktuální tabulkou, pravidly a místy, kde lidé rozhodnutí opravují. Společně určíme, zda má být první matematické modelování, automatizace pravidel, nebo prototyp.

Prověřit provozní problém Zobrazit prototyp

Snímek zdrojů / 2026-06-21

Tvrzení o NPA vycházejí ze snímku repozitáře finitefield-org/npa. Postavení Lean a Rocq vychází z jejich oficiálních webů. Stav repozitářů, nejnovější tagy a formulace revize metody byly zkontrolovány 2026-06-28.