01 / Grens
Houd de vertrouwde basis klein
AI, tactieken en zoeken helpen kandidaten te maken, maar het eindbewijs moet onafhankelijk worden gecontroleerd.
Finite Field / Math Lab
Bouw bewijs voor correctheid, niet alleen snelle resultaten.
Math Lab laat zien hoe we omgaan met wiskundige modellering, bewijsassistenten, formele verificatie, reproduceerbaarheid en vertrouwde implementatie, zonder het bewijs sterker voor te stellen dan het is.
- Publieke projecten
- NPA / STD / MATHLIB
- Kerntaal
- Rust
- NPA-snapshot
- v0.1.1
Bewijsaudit / conceptueel overzicht
Alleen lezen
01 canonieke bytes / formaat OK
02 certificaathash OK
03 controle van afhankelijke bewijzen OK
04 bronvrij oordeel OK
Vertrouwensgrens zichtbaar
Deze pagina beweert niet dat NPA een praktische vervanging is voor Lean of Rocq, en de browsersimulatie voert NPA niet uit.
Labprincipe
Publiceer niet alleen resultaten, maar ook de grens van controle.
Een conclusie zoals “het werkte”, “het was snel” of “het is bewezen” is niet genoeg. We tonen invoer, aannames, vertrouwde delen, onafhankelijk controleerbare artefacten en open kwesties apart.
02 / Bewijs
Maak bewijs een artefact
Laat certificaten, hashes, aannamelijsten, benchmarkvoorwaarden en logs achter in een vorm die anderen kunnen inspecteren.
03 / Reproduceer
Ontwerp voor reproduceerbaarheid
Leg toolchains, invoerdata, uitvoeringsopdrachten en criteria vast zodat het resultaat opnieuw gecontroleerd kan worden.
04 / Eerlijkheid
Overdrijf de onderzoeksstatus niet
Toon praktische methoden, experimenten en onderzoek apart. Zet beperkingen naast resultaten.
METHODEBEOORDELING
Een categorie voor servicemethoden die nog reikwijdte, verantwoordelijkheid, klantbewijs en goedkeuring nodig heeft voordat ze projectklaar genoemd mag worden.
EXPERIMENTEEL
Er bestaat een werkende implementatie, maar schaal, compatibiliteit, prestaties of specificatiewijzigingen kunnen nog veranderen. Versie en reproductiestappen zijn verplicht.
ONDERZOEK
Ontwerp, evaluatie, bewijs of implementatie loopt nog. Dit impliceert geen commerciële beschikbaarheid of voltooiing.
Onderzoeksportfolio
Bekijk onderzoek op volwassenheid en artefacten.
Elke kaart toont volwassenheid, artefacten, huidige staat en volgende validatie. Zoeken en filters gebruiken alleen browserstatus.
8 getoond
EXPERIMENTEEL
OPEN SOURCE
01
Nano Proof Auditor
Toolchain voor bewijzen met certificaten als uitgangspunt
Een onderzoekstoolchain die canonieke bewijscertificaten en een kleine controlebasis centraal zet in de beoordeling van afhankelijke bewijzen.
- Artefacten
- broncode / specificatie / CI-sjablonen
- Huidig
- openbare snapshot v0.1.1
- Volgende validatie
- externe stellingpakketten en onafhankelijke controle
EXPERIMENTEEL
OPEN SOURCE
02
NPA Standard Library
Logic / Nat / List / Algebra
Een standaardrepository met stellingpakketten voor herbruikbare NPA-basiscomponenten.
- Artefacten
- broncode / bewijspakketten
- Huidig
- openbare gesplitste repository
- Volgende validatie
- pakketbereik en compatibiliteit
ONDERZOEK
OPEN SOURCE
03
NPA Math Library
Formele wiskundebibliotheek
Een bibliotheekrichting voor het opslaan van wiskundige stellingen als onafhankelijk controleerbare bewijspakketten.
- Artefacten
- broncode / bewijspakketten
- Huidig
- openbare repository in ontwikkeling
- Volgende validatie
- bibliotheekstructuur en afhankelijkheidsaudit
METHODEBEOORDELING
METHODE
04
Planningsmodellen met randvoorwaarden
Roosters / routes / toewijzing
Een methode om harde randvoorwaarden en evaluatiemaatstaven te scheiden in werk rond diensten, bezoeken, routes, productie en toewijzing.
- Artefacten
- model / prototype / toelichtingsrapport
- Huidig
- servicemethode; openbare claim beperkt tot methodebeoordeling
- Volgende validatie
- klantbewijs en goedkeuring van de reikwijdte
ONDERZOEK
METING
05
Reproduceerbare solverevaluatie
Benchmark en bewijs
Een programma om instantiesets, hardware, tijdslimieten, willekeurige seeds en ruwe logs vast te leggen voordat prestatieclaims worden gedaan.
- Artefacten
- benchmarkregister / ruwe logs / rapport
- Huidig
- ontwerp van onderzoeksprogramma
- Volgende validatie
- eerste openbare benchmarkcorpus
ONDERZOEK
FORMELE METHODEN
06
Verificatie voor kritieke bedrijfslogica
Invarianten voor bedrijfssystemen
Onderzoek naar het scheiden van tarieven, rechten, voorraad en statusovergangen in specificaties en invarianten.
- Artefacten
- specificatie / invarianten / test- of bewijsrapport
- Huidig
- reikwijdtestudie
- Volgende validatie
- één begrensde productieachtige casus selecteren
EXPERIMENTEEL
ENGINEERING
07
Kleine vertrouwde componenten in Rust
Kleine vertrouwde componenten
Implementatiewerk dat vertrouwenskritieke onderdelen zoals checkers en hashes klein genoeg houdt om te inspecteren.
- Artefacten
- NPA-kernel / certificaatcrate / referentiechecker
- Huidig
- openbare implementatie in NPA
- Volgende validatie
- compatibiliteit met onafhankelijke checker
ONDERZOEK
AI × BEWIJS
08
AI-ondersteuning en onafhankelijke controle
Vrij genereren, strikt verifiëren
AI, tactieken en zoeken helpen kandidaten te maken, maar het eindbewijs moet onafhankelijk worden gecontroleerd.
- Artefacten
- kandidaatgenerator / certificaat / checkerrapport
- Huidig
- onderzoeksrichting volgens het vertrouwensmodel van NPA
- Volgende validatie
- gemeten werkwijze voor auteurs
Geen passend onderzoeksgebied gevonden.
Probeer een ander trefwoord of zet het volwassenheidsfilter terug op alles.
Nano Proof Auditor
Scheid bewijsgeneratie van wat we vertrouwen.
AI, tactieken en zoeken helpen kandidaten te maken, maar het eindbewijs moet onafhankelijk worden gecontroleerd.
EXPERIMENTEELOPEN SOURCEAPACHE-2.0
Huidige snapshot
v0.1.1
Openbare informatie gecontroleerd op 2026-06-21.
Primaire kern
Rust
Rust-verifier en kernel horen bij de controlezijde.
Audit-artefact
.npcert
Canonieke certificaatbytes zijn het te inspecteren object.
Hercontrolepunt
handmatige beoordeling
Repositorystatus en zichtbaarheid van pakketten moeten vóór publicatie worden beoordeeld.
Verkenner voor vertrouwensgrenzen
Klik door wat vertrouwd is en wat niet.
Klik op elk knooppunt om te zien wat het doet, wat het produceert en welke controle nog vereist is.
UNTRUSTED
CHECKED
Belangrijke grens
NPA is momenteel geen praktische vervanging voor Lean of Rocq. Deze pagina legt certificaatgericht onderzoeksontwerp uit en garandeert geen foutloze commerciële systemen of automatisch bewijzen van stellingen.
Certificaatcontrole / uitlegsimulatie
Ervaar de stroom van certificaatcontrole.
De browserinteractie legt de inspectiestroom uit. Ze voert geen NPA, Rust, WASM of echte bewijscertificaten uit.
CLI-voorbeeld
npa package verify-certs --root . --checker reference --json
NPA / audit trace
READY
- 01 Lees het certificaatcanonieke bytes / formaat WAIT
- 02 Controleer de certificaathashcertificaathash WAIT
- 03 Controleer met de kernelcontrole van afhankelijke bewijzen WAIT
- 04 Controleer opnieuw met de referentiecheckerbronvrij oordeel WAIT
- 05 Vergelijk het axiomarapporthash van axiomarapport WAIT
Oordeel
De uitleg is nog niet uitgevoerd.Voer de uitleg uit om de stappen op volgorde te visualiseren.
Bewijsecosysteem
Maak rollen duidelijk in plaats van hulpmiddelen te rangschikken.
Lean en Rocq zijn volwassen ecosystemen voor bewijsassistenten. NPA wordt hier getoond als certificaatgericht onderzoeks- en implementatieproject, niet als vervangingsranglijst.
| Onderdeel | Lean | Rocq | NPA |
|---|---|---|---|
| Positie | Open-source programmeertaal en bewijsassistent. | Interactieve stellingbewijzer met een lange onderzoeksgeschiedenis. | Onderzoeks- en implementatierepository voor certificaatgerichte controle. |
| Typisch gebruik | Wiskunde, softwareverificatie en programmeren. | Wiskunde, specificaties, programmaverificatie en extractie. | Onderzoek naar bewijscertificaten en onafhankelijke controle. |
| Nadruk | Uitbreidbaarheid, bibliotheken en interactief bewijzen. | Expressiviteit, volwassen methoden en bibliotheken. | Kleine vertrouwde basis en canonieke certificaten. |
| Hoe deze pagina dit behandelt | Referentie voor leren, vergelijken en interoperabiliteit. | Referentie voor leren, vergelijken en formalisatiemethoden. | Onderzoeksproject van Finite Field. |
| Grens | Specialistische kennis blijft nodig. | Specialistische kennis blijft nodig. | Momenteel niet bedoeld als praktische vervanging voor Lean of Rocq. |
Onderzoeksmethode
Maak van “het werkte” een herhaalbare controleprocedure.
Een resultaat wordt sterker wanneer iemand het onder dezelfde voorwaarden opnieuw kan uitvoeren, inspecteren en afwijzen.
Vraag
Definieer wat moet worden gecontroleerd: prestaties, correctheid, compatibiliteit of reikwijdte.
Aannames
Schrijf aannames, uitsluitingen, axioma's, datalacunes en bias op vóór de evaluatie.
Artefact
Bewaar broncode, certificaten, invoer, uitvoeringslogs en hashes.
Onafhankelijke controle
Controleer resultaten via een ander pad dan de generatiezijde.
Vergelijkingstest
Leg hardware, versies, tijdslimieten, instantiesets en willekeurige seeds vast.
Grenzen
Publiceer mislukkingen, niet-ondersteunde gevallen, prestatiegrenzen en de volgende validatie.
Reproduceerbaarheidsbouwer
Controleer wat een onderzoekspublicatie nog mist.
De checklist wordt alleen in de browser verwerkt. Het is geen certificeringsscore.
Gereedheid
0%Volgende actie
Definieer eerst de onderzoeksvraag en succesvoorwaarde.Voordat artefactformaten worden gekozen, moet vaststaan wat wordt vergeleken of gecontroleerd.
Openbare artefacten
Volg openbare artefacten vanuit één ingang.
De pagina vermijdt runtime-aanroepen naar de GitHub API. De repositorystatus is een beoordeelde snapshot die vóór publicatie opnieuw moet worden gecontroleerd.
4 artefacten
finitefield-org
npa
toolchain voor bewijzen met certificaten als uitgangspunt
VERIFY
package verify-certs
finitefield-org
npa-std
standaardpakket met stellingen
ROLE
Std.Logic / Nat / List
finitefield-org
npa-mathlib
formele wiskundebibliotheek
ROLE
formal theorem packages
GitHub
finitefield-org
index van openbare repositories
INDEX
alle openbare repositories
Geen openbaar artefact komt overeen met de zoekopdracht.
Publicatiebeleid
Openbare repositories, onderzoeksnotities en benchmarks moeten de controledatum, volwassenheid, reproductiestappen en bekende beperkingen vermelden. Sterren en commit-aantallen worden niet getoond als signalen voor onderzoekskwaliteit.
Van Lab naar operatie
Breng onderzoeksdiscipline in het ontwerp van bedrijfssystemen.
Niet elk klantsysteem heeft bewijsassistenten nodig. De bruikbare overdracht is bepalen wat mensen moeten vertrouwen, vergelijken, controleren, corrigeren en goedkeuren.
Labpraktijk
Scheid generatie, berekening en eindcontrole in plaats van elke laag evenveel te vertrouwen.
Bewaar invoer, uitvoer, certificaten, hashes en logs als beoordeelbare artefacten.
Leg data, versies, opdrachten en evaluatiecriteria vast voordat resultaten worden vergeleken.
Publiceer randvoorwaarden, mislukte gevallen en open punten met hetzelfde gewicht als resultaten.
Klantsysteem
Definieer wie invoert, wie beoordeelt, wie handmatig overschrijft en wie het resultaat bevestigt.
Toon randvoorwaarden, evaluatiescores, afgewezen kandidaten en open punten.
Bewaar wijzigingen in voorwaarden, berekeningsruns en de geschiedenis van eindgoedkeuring.
Maak automatische uitvoer corrigeerbaar, afwijsbaar en uitlegbaar voor operators.
01
Diensten en personeelsbezetting
Toon regelovertredingen en mate van voorkeurvervulling apart.
02 VoertuigrouteringHoud routeredenen, capaciteit, tijdvensters en uitzonderingen zichtbaar.
03 ProductieplanningLeg ongepland werk, knelpunten en afwegingen rond omstellen uit.
04 Toewijzing en matchingToon kandidaatredenen en alternatieven voordat goedkeuring plaatsvindt.
Onderzoeksnotities
Houd updategeschiedenis en bewijs leesbaar.
Niet elke kaart is een gepubliceerd artikel. Notities in voorbereiding blijven zonder publicatielabel totdat ze datums, bronnen en reproductiestappen hebben.
NPA / Current
Waarom certificaten centraal staan
Waarom eindbewijs een gestandaardiseerd certificaat moet zijn dat via een klein onafhankelijk pad wordt gecontroleerd.
Open de openbare repositoryDesign note / planned
Optimalisatieresultaten uitlegbaar maken
Een ontwerpnotitie over het zichtbaar maken van doelstellingen, harde randvoorwaarden, zachte voorkeuren en onopgeloste toewijzingen in de UI.
Bekijk gerelateerde demo'sBenchmark / planned
Voorwaarden voor eerlijke solververgelijking
Een geplande notitie over instantiesets, tijdslimieten, optimaliteitskloven, willekeurige seeds en hardware.
Bekijk publicatiecriteriaItems met “In voorbereiding” zijn geen gepubliceerde artikelen. Na publicatie krijgt elke notitie een datum, bron, auteur, reproductiepad en bekende beperkingen.
FAQ
Grenzen tussen onderzoek, bewijshulpmiddelen en zakelijk gebruik.
Deze punten worden expliciet gemaakt voordat onderzoekspagina's worden aangezien voor productiegaranties.
Over het bedrijf lezen01 Is Math Lab een ontwikkelservice op contractbasis?
Nee. Het is een plek om onderzoeksaanpak en artefacten te publiceren. In klantgesprekken scheiden we toepasbare methoden, methoden die meer validatie vereisen en onderzoeksthema’s.
02 Kan NPA Lean of Rocq vervangen?
Nee. Het huidige NPA is geen praktische vervanging voor Lean of Rocq. Het is een onderzoeks- en implementatieproject rond certificaten, onafhankelijke controle en een kleine vertrouwde basis.
03 Vertrouwen jullie AI-gegenereerde bewijzen zoals ze zijn?
Nee. AI, zoeken en tactieken helpen kandidaten te genereren. Wij kijken of het eindcertificaat wordt geaccepteerd door een checker die onafhankelijk is van die generatiepaden.
04 Verwijdert formele verificatie alle fouten?
Nee. Formele methoden controleren specifieke eigenschappen tegen een expliciete specificatie. Verkeerde specificaties, code buiten de reikwijdte, operaties en externe diensten vereisen nog steeds aparte beoordeling.
05 Heeft dit verband met werk aan bedrijfssystemen?
Ja. Meestal passen we de discipline geleidelijk toe: randvoorwaarden, resultaatredenen, berekeningsgeschiedenis, toestemmingsgrenzen en controles voor belangrijke bedrijfslogica.
Bespreek een probleem
U kunt het werk bespreken dat opgelost moet worden, niet alleen het onderzoeksthema.
Begin bij de huidige spreadsheet, regels en plaatsen waar mensen beslissingen corrigeren. We kunnen ordenen of wiskundige modellering, regelautomatisering of een prototype eerst moet komen.
Bronsnapshot / 2026-06-21
NPA-claims zijn gebaseerd op de snapshot van de finitefield-org/npa-repository. De positionering van Lean en Rocq is gebaseerd op hun officiële sites. Repositorystatus, nieuwste tags en formuleringen rond methodebeoordeling zijn gecontroleerd op 2026-06-28.