01 / Grænse
Hold den betroede base lille
Placer ikke komplekse generatorer eller AI i centrum for tilliden. Gør den lille kontrolside eksplicit.
Finite Field / Math Lab
Byg dokumentation for korrekthed, ikke kun hurtige resultater.
Math Lab viser, hvordan vi håndterer matematisk modellering, teorembevisning, formel verifikation, reproducerbarhed og betroet implementering uden at overdrive dokumentationen.
- Offentlige projekter
- NPA / STD / MATHLIB
- Kernesprog
- Rust
- NPA-snapshot
- v0.1.1
Bevisrevision / konceptvisning
Kun læsning
01 kanoniske bytes / format OK
02 certificate_hash OK
03 afhængig beviskontrol OK
04 kildefri afgørelse OK
Tillidsgrænsen er synlig
Denne side hævder ikke, at NPA er en praktisk erstatning for Lean eller Rocq, og browsersimulationen kører ikke NPA.
Lab-princip
Udgiv ikke kun resultater, men også grænsen for kontrol.
En konklusion som “det virkede”, “det var hurtigt” eller “det blev bevist” er ikke nok. Vi viser inddata, antagelser, betroede dele, uafhængigt kontrollerbare artefakter og uløste spørgsmål hver for sig.
02 / Dokumentation
Gør dokumentation til et artefakt
Efterlad certifikater, hashes, antagelseslister, benchmarkbetingelser og logfiler i en form, andre kan inspicere.
03 / Reproducerbarhed
Design til reproducerbarhed
Fastlås værktøjskæder, inputdata, kørselskommandoer og kriterier, så resultatet kan kontrolleres igen.
04 / Ærlighed
Overdriv ikke forskningsstatus
Vis praktiske metoder, eksperimenter og forskning hver for sig. Placer begrænsninger ved siden af resultaterne.
METODEGENNEMGANG
En kategori for servicemetoder, der stadig kræver afgrænsning, ansvar, kundedokumentation og godkendelse, før den kan beskrives som projektklar.
EKSPERIMENTELT
Der findes en fungerende implementering, men skala, kompatibilitet, ydeevne eller specifikation kan stadig ændre sig. Version og reproduktionstrin er nødvendige.
FORSKNING
Design, evaluering, bevis eller implementering er i gang. Det betyder ikke, at løsningen er kommercielt tilgængelig eller færdig.
Forskningsportefølje
Se forskning efter modenhed og artefakter.
Hvert kort viser modenhed, artefakter, aktuel tilstand og næste validering. Søgning og filtre bruger kun tilstand i browseren.
8 vist
EKSPERIMENTELT
OPEN SOURCE
01
Nano Proof Auditor
Certifikatbaseret værktøjskæde til beviser
En forskningsværktøjskæde, der placerer kanoniske beviscertifikater og en lille kontrolbase i centrum for gennemgang af afhængige beviser.
- Artefakter
- kilde / specifikation / CI-skabeloner
- Aktuelt
- offentligt v0.1.1-snapshot
- Næste validering
- eksterne teorempakker og uafhængig kontrol
EKSPERIMENTELT
OPEN SOURCE
02
NPA Standard Library
Logik / Nat / List / Algebra
Et standardrepository med teorempakker til genbrugelige NPA-fundamenter.
- Artefakter
- kilde / bevispakker
- Aktuelt
- offentligt opdelt repository
- Næste validering
- pakkeafgrænsning og kompatibilitet
FORSKNING
OPEN SOURCE
03
NPA Math Library
Formelt matematikbibliotek
En biblioteksretning til at lagre matematiske teoremer som uafhængigt kontrollerbare bevispakker.
- Artefakter
- kilde / bevispakker
- Aktuelt
- offentligt repository under udvikling
- Næste validering
- biblioteksstruktur og afhængighedsrevision
METODEGENNEMGANG
METODE
04
Planlægningsmodeller med begrænsninger
Planlægning / ruter / tildeling
En metode til at adskille hårde begrænsninger og evalueringsmål i arbejde med vagter, besøg, ruter, produktion og tildeling.
- Artefakter
- model / prototype / forklaringsrapport
- Aktuelt
- servicemetode; offentlig påstand begrænset til metodegennemgang
- Næste validering
- kundedokumentation og godkendt afgrænsning
FORSKNING
MÅLING
05
Reproducerbar evaluering af solvere
Benchmark og dokumentation
Et program til at fastlåse instanssæt, hardware, tidsgrænser, tilfældighedsfrø og rå logfiler, før der fremsættes påstande om ydeevne.
- Artefakter
- benchmarkregister / rå logfiler / rapport
- Aktuelt
- design af forskningsprogram
- Næste validering
- første offentlige benchmarkkorpus
FORSKNING
FORMELLE METODER
06
Verifikation af kritisk forretningslogik
Invarianter for forretningssystemer
Forskning i at adskille gebyrer, tilladelser, lager og tilstandsovergange i specifikationer og invarianter.
- Artefakter
- specifikation / invarianter / test- eller bevisrapport
- Aktuelt
- afgrænsningsundersøgelse
- Næste validering
- vælg ét afgrænset produktionslignende tilfælde
EKSPERIMENTELT
TEKNIK
07
Små betroede komponenter i Rust
Små betroede komponenter
Implementeringsarbejde, der holder tillidskritiske dele som kontroller og hashes små nok til at kunne inspiceres.
- Artefakter
- NPA-kerne / certifikatkomponent / referencekontrol
- Aktuelt
- offentlig implementering i NPA
- Næste validering
- kompatibilitet med uafhængig kontrol
FORSKNING
AI × BEVIS
08
AI-assistance og uafhængig kontrol
Generér frit, verificér strengt
En forskningsretning, der placerer AI på kandidatgenereringen, mens den endelige dokumentation kontrolleres uafhængigt.
- Artefakter
- kandidatgenerator / certifikat / kontrolrapport
- Aktuelt
- forskningsretning i tråd med NPA's tillidsmodel
- Næste validering
- målt forfatterworkflow
Der blev ikke fundet et matchende forskningsområde.
Prøv et andet søgeord, eller sæt modenhedsfilteret tilbage til alle.
Nano Proof Auditor
Adskil bevisgenerering fra det, vi stoler på.
NPA er en certifikatbaseret værktøjskæde til afhængige beviser. Frontender, taktikker, teoremsøgning, plugins, AI, kildefiler og CI-status kan hjælpe med at skabe kandidater, men de er ikke den betroede bevisdokumentation.
EKSPERIMENTELTOPEN SOURCEAPACHE-2.0
Aktuelt snapshot
v0.1.1
Offentlig information kontrolleret 2026-06-21.
Primær kerne
Rust
Rust-verifikator og kerne er en del af kontrolsiden.
Revisionsartefakt
.npcert
Kanoniske certifikat-bytes er objektet, der skal inspiceres.
Genkontrolpunkt
manuel gennemgang
Repositoriets tilstand og pakkernes synlighed skal gennemgås før udgivelse.
Udforsk tillidsgrænsen
Klik dig igennem, hvad der er betroet, og hvad der ikke er.
Klik på hver node for at undersøge, hvad den gør, hvad den producerer, og hvilken kontrol der stadig er nødvendig.
IKKE BETROET
KONTROLLERET
Vigtig grænse
NPA er i øjeblikket ikke en praktisk erstatning for Lean eller Rocq. Denne side forklarer certifikatcentreret forskningsdesign og garanterer ikke fejlfrie kommercielle systemer eller automatisk teoremløsning.
Certifikatkontrol / forklarende simulation
Oplev forløbet for certifikatkontrol.
Browserinteraktionen forklarer kontrolforløbet. Den kører ikke NPA, Rust, WASM eller rigtige beviscertifikater.
CLI-eksempel
npa package verify-certs --root . --checker reference --json
NPA / revisionsspor
KLAR
- 01 Læs certifikatetkanoniske bytes / format VENT
- 02 Kontrollér certifikatets hashcertificate_hash VENT
- 03 Kontrollér med kernenafhængig beviskontrol VENT
- 04 Kontrollér igen med referencekontrollenkildefri afgørelse VENT
- 05 Sammenlign aksiomrapportenaksiomrapport-hash VENT
Afgørelse
Forklaringen er ikke kørt endnu.Kør forklaringen for at visualisere trinene i rækkefølge.
Bevisøkosystem
Afklar roller i stedet for at rangordne værktøjer.
Lean og Rocq er modne økosystemer for bevisassistenter. NPA vises her som et certifikatcentreret forsknings- og implementeringsprojekt, ikke som en erstatningsrangliste.
| Emne | Lean | Rocq | NPA |
|---|---|---|---|
| Position | Open source-programmeringssprog og bevisassistent. | Interaktiv teorembeviser med lang forskningshistorik. | Forsknings- og implementeringsrepository til certifikatbaseret kontrol. |
| Typisk anvendelse | Matematik, softwareverifikation og programmering. | Matematik, specifikationer, programverifikation og ekstraktion. | Forskning i beviscertifikater og uafhængig kontrol. |
| Fokus | Udvidelsesmuligheder, biblioteker og interaktiv bevisførelse. | Udtrykskraft, modne metoder og biblioteker. | Lille tillidsbase og kanoniske certifikater. |
| Sådan behandles det på siden | Reference til læring, sammenligning og interoperabilitet. | Reference til læring, sammenligning og formaliseringsmetoder. | Finite Field-forskningsprojekt. |
| Grænse | Specialistviden er stadig nødvendig. | Specialistviden er stadig nødvendig. | Ikke tænkt som en praktisk erstatning for Lean eller Rocq på nuværende tidspunkt. |
Forskningsmetode
Gør “det virkede” til en gentagelig kontrolprocedure.
Et resultat bliver stærkere, når andre kan køre det igen, inspicere det og afvise det under samme betingelser.
Spørgsmål
Definér, hvad der skal kontrolleres: ydeevne, korrekthed, kompatibilitet eller scope.
Antagelser
Skriv antagelser, undtagelser, aksiomer, datahuller og bias ned før evaluering.
Artefakt
Bevar kilde, certifikater, inddata, kørselslogfiler og hashes.
Uafhængig kontrol
Kontrollér resultater gennem en anden vej end genereringssiden.
Benchmark
Fastlås hardware, versioner, tidsgrænser, instanssæt og tilfældighedsfrø.
Begrænsninger
Udgiv fejl, ikke-understøttede tilfælde, ydelsesgrænser og næste validering.
Reproducerbarhedsbygger
Tjek, hvad en forskningsudgivelse stadig mangler.
Tjeklisten behandles kun i browseren. Den er ikke en certificeringsscore.
Klarhed
0%Næste handling
Definér først forskningsspørgsmålet og succeskriteriet.Før artefaktformater vælges, skal det fastlægges, hvad der skal sammenlignes eller kontrolleres.
Offentlige artefakter
Saml offentlige artefakter ét sted.
Siden undgår runtime-kald til GitHub API. Repositoriets tilstand er et gennemgået snapshot, der skal kontrolleres før udgivelse.
4 artefakter
finitefield-org
npa
certifikatbaseret værktøjskæde til beviser
KONTROL
package verify-certs
finitefield-org
npa-std
standardteorempakke
ROLLE
Std.Logic / Nat / List
finitefield-org
npa-mathlib
formelt matematikbibliotek
ROLLE
formelle teorempakker
GitHub
finitefield-org
offentligt repositoryindeks
INDEKS
alle offentlige repositories
Ingen offentlige artefakter matcher søgningen.
Udgivelsespolitik
Offentlige repositories, forskningsnoter og benchmarks bør have kontrolleret dato, modenhed, reproduktionstrin og kendte begrænsninger. Stjerner og commit-antal vises ikke som signaler for forskningskvalitet.
Fra Lab til drift
Bring forskningsdisciplin ind i designet af forretningssystemer.
Ikke alle kundesystemer har brug for teorembevisning. Det nyttige er at afgøre, hvad der skal betros, sammenlignes, kontrolleres, rettes og godkendes af mennesker.
Lab-praksis
Adskil generering, beregning og endelig kontrol i stedet for at stole lige meget på alle lag.
Bevar inddata, uddata, certifikater, hashes og logfiler som artefakter, der kan gennemgås.
Fastlås data, versioner, kommandoer og evalueringskriterier, før resultater sammenlignes.
Udgiv begrænsninger, fejlede tilfælde og uløste punkter med samme vægt som resultater.
Kundesystem
Definér, hvem der indtaster, hvem der gennemgår, hvem der tilsidesætter, og hvem der bekræfter resultatet.
Vis begrænsninger, evalueringsscore, afviste kandidater og uløste punkter.
Bevar ændringer i betingelser, beregningskørsler og den endelige godkendelseshistorik.
Gør automatiske resultater mulige at rette, afvise og forklare for operatører.
01
Vagter og bemanding
Vis regelbrud og opfyldelse af præferencer hver for sig.
02 Ruteplanlægning for køretøjerHold rutebegrundelser, kapacitet, tidsvinduer og undtagelser synlige.
03 ProduktionsplanlægningForklar ikke-planlagt arbejde, flaskehalse og afvejninger ved omstilling.
04 Tildeling og matchningVis kandidatbegrundelser og alternativer før godkendelse.
Forskningsnoter
Hold opdateringshistorik og dokumentation læsbar.
Ikke alle kort er publicerede artikler. Forberedende noter markeres ikke som publiceret arbejde, før de har datoer, kilder og reproduktionstrin.
NPA / Aktuelt
Hvorfor placere certifikater i centrum
Hvorfor den endelige dokumentation bør være et standardiseret certifikat, der kontrolleres gennem en lille uafhængig vej.
Vis offentligt repositoryDesignnotat / planlagt
Gør optimeringsresultater forklarlige
Et designnotat om at vise mål, hårde begrænsninger, bløde præferencer og uløste tildelinger i UI.
Se relaterede demoerBenchmark / planlagt
Betingelser for fair sammenligning af solvere
En planlagt note om instanssæt, tidsgrænser, optimalitetsgab, tilfældighedsfrø og hardware.
Se udgivelseskriterierElementer under “Under forberedelse” er ikke publicerede artikler. Efter udgivelse får hver note dato, kilde, forfatter, reproduktionsvej og kendte begrænsninger.
FAQ
Grænser for forskning, bevisværktøjer og brug i forretningen.
Disse punkter gøres eksplicitte, før forskningssider forveksles med produktionsgarantier.
Læs om virksomheden01 Er Math Lab en kontraktudviklingstjeneste?
Nej. Det er et sted til at offentliggøre forskningsholdning og artefakter. I kundedialoger skelner vi mellem anvendelige metoder, metoder der kræver mere validering, og emner på forskningsstadiet.
02 Kan NPA erstatte Lean eller Rocq?
Nej. Den nuværende NPA er ikke en praktisk erstatning for Lean eller Rocq. Det er et forsknings- og implementeringsprojekt om certifikater, uafhængig kontrol og en lille tillidsbase.
03 Stoler I på AI-genererede beviser, som de er?
Nej. AI, søgning og taktikker hjælper med at generere kandidater. Vi fokuserer på, om det endelige certifikat accepteres af en kontrol, der er uafhængig af disse genereringsveje.
04 Fjerner formel verifikation alle fejl?
Nej. Formelle metoder kontrollerer bestemte egenskaber mod en eksplicit specifikation. Forkerte specifikationer, kode uden for scope, drift og eksterne tjenester kræver stadig særskilt gennemgang.
05 Har det betydning for arbejdet med forretningssystemer?
Ja. Vi anvender normalt disciplinen gradvist: begrænsninger, resultatårsager, beregningshistorik, tilladelsesgrænser og kontroller af vigtig forretningslogik.
Drøft et problem
I kan drøfte det arbejde, der skal løses, ikke kun forskningsemnet.
Begynd med det nuværende regneark, reglerne og de steder, hvor mennesker retter beslutninger. Vi kan afklare, om matematisk modellering, regelautomatisering eller en prototype bør komme først.
Kildesnapshot / 2026-06-21
NPA-påstande bygger på snapshot af finitefield-org/npa-repositoriet. Positioneringen af Lean og Rocq bygger på deres officielle websteder. Repositoriets tilstand, seneste tags og formuleringer om metodegennemgang blev kontrolleret 2026-06-28.