01 / Gräns
Håll den betrodda basen liten
Placera inte komplexa generatorer eller AI i centrum för förtroendet. Gör den lilla kontrollsidan explicit.
Finite Field / Matematiklabb
Skapa belägg för korrekthet,inte bara snabba resultat.
Matematiklabbet visar hur vi hanterar matematisk modellering, teorembevisning, formell verifiering, reproducerbarhet och betrodd implementation utan att överdriva bevisläget.
- Offentliga projekt
- NPA / STD / MATHLIB
- Kärnspråk
- Rust
- NPA-ögonblicksbild
- v0.1.1
Bevisgranskning / konceptvy
Endast läsning
01 kanoniska byte / format OK
02 certifikatets hash OK
03 kontroll av beroende bevis OK
04 källoberoende utlåtande OK
Förtroendegränsen är synlig
Den här sidan påstår inte att NPA är en praktisk ersättning för Lean eller Rocq, och webbläsarsimuleringen kör inte NPA.
Labbprincip
Publicera inte bara resultat, utan även kontrollgränsen.
En slutsats som 'det fungerade', 'det var snabbt' eller 'det är bevisat' räcker inte. Vi visar indata, antaganden, betrodda delar, oberoende kontrollerbara artefakter och olösta frågor separat.
02 / Bevisning
Gör bevis till en artefakt
Lämna certifikat, hashvärden, antagandelistor, benchmarkvillkor och loggar i en form som andra kan granska.
03 / Reproducera
Designa för reproducerbarhet
Lås verktygskedjor, indata, körkommandon och kriterier så att resultatet kan kontrolleras igen.
04 / Ärlighet
Överdriv inte forskningsstatus
Visa praktiska metoder, experiment och forskning separat. Placera begränsningar bredvid resultaten.
METODGRANSKNING
En metodkategori för tjänster som fortfarande kräver omfattning, ansvar, kundunderlag och godkännande innan den beskrivs som projektklar.
EXPERIMENTELL
En fungerande implementation finns, men skala, kompatibilitet, prestanda eller specifikationsändringar kan fortfarande återstå. Version och reproduktionssteg krävs.
FORSKNING
Design, utvärdering, bevis eller implementation pågår. Detta innebär inte kommersiell tillgänglighet eller färdigställande.
Forskningsportfölj
Visa forskning efter mognad och artefakter.
Varje kort visar mognad, artefakter, aktuellt läge och nästa validering. Sökning och filter använder endast webbläsarens lokala tillstånd.
8 visas
EXPERIMENTELL
ÖPPEN KÄLLKOD
01
Nano Proof Auditor
Bevisverktygskedja med certifikat först
En forskningsverktygskedja som placerar kanoniska beviscertifikat och en liten kontrollbas i centrum för granskning av beroende bevis.
- Artefakter
- källkod / specifikation / CI-mallar
- Nuvarande
- offentlig ögonblicksbild v0.1.1
- Nästa validering
- externa teorempaket och oberoende kontroll
EXPERIMENTELL
ÖPPEN KÄLLKOD
02
NPA Standard Library
Logic / Nat / List / Algebra
Ett standardrepository för teorempaket med återanvändbara NPA-grunder.
- Artefakter
- källkod / bevispaket
- Nuvarande
- offentligt delat repository
- Nästa validering
- paketomfattning och kompatibilitet
FORSKNING
ÖPPEN KÄLLKOD
03
NPA Math Library
Formellt matematikbibliotek
En biblioteksinriktning för att lagra matematiska teorem som oberoende kontrollerbara bevispaket.
- Artefakter
- källkod / bevispaket
- Nuvarande
- offentligt repository under utveckling
- Nästa validering
- biblioteksstruktur och beroendegranskning
METODGRANSKNING
METOD
04
Planeringsmodeller med begränsningar
Schemaläggning / ruttning / tilldelning
En metod för att separera hårda begränsningar och utvärderingsmått i skift, besök, rutter, produktion och tilldelningsarbete.
- Artefakter
- modell / prototyp / förklaringsrapport
- Nuvarande
- tjänstemetod; offentligt påstående begränsat till metodgranskning
- Nästa validering
- kundunderlag och godkänd omfattning
FORSKNING
MÄTNING
05
Reproducerbar utvärdering av lösare
Jämförelsetest och bevisning
Ett program för att låsa instansuppsättningar, hårdvara, tidsgränser, slumpfrön och råloggar innan prestandapåståenden görs.
- Artefakter
- benchmarkregister / råloggar / rapport
- Nuvarande
- design av forskningsprogram
- Nästa validering
- första offentliga benchmarkkorpus
FORSKNING
FORMELLA METODER
06
Verifiering av kritisk verksamhetslogik
Invarianter för verksamhetssystem
Forskning om att separera avgifter, behörigheter, lager och tillståndsövergångar till specifikationer och invarianter.
- Artefakter
- specifikation / invarianter / test- eller bevisrapport
- Nuvarande
- omfattningsstudie
- Nästa validering
- välj ett avgränsat produktionsliknande fall
EXPERIMENTELL
TEKNIK
07
Små betrodda komponenter i Rust
Små betrodda komponenter
Implementeringsarbete som håller förtroendekritiska delar som kontroller och hashfunktioner små nog att granska.
- Artefakter
- NPA-kärna / certifikat-crate / referenskontroll
- Nuvarande
- offentlig implementation i NPA
- Nästa validering
- kompatibilitet med oberoende kontroll
FORSKNING
AI × BEVIS
08
AI-stöd och oberoende kontroll
Generera fritt, verifiera strikt
En forskningsinriktning som placerar AI på kandidatgenerering medan den slutliga bevisningen kontrolleras oberoende.
- Artefakter
- kandidatgenerator / certifikat / kontrollrapport
- Nuvarande
- forskningsinriktning i linje med NPA:s förtroendemodell
- Nästa validering
- uppmätt arbetsflöde för författande
Inget matchande forskningsområde hittades.
Prova ett annat sökord eller återställ mognadsfiltret till alla.
Nano Proof Auditor
Separera bevisgenerering från det vi litar på.
NPA är en certifikatförst-verktygskedja för beroende bevis. Gränssnitt, taktiker, teoremsökning, tillägg, AI, källfiler och CI-status kan hjälpa till att skapa kandidater, men de är inte den betrodda bevisningen.
EXPERIMENTELLÖPPEN KÄLLKODAPACHE-2.0
Aktuell ögonblicksbild
v0.1.1
Offentlig information kontrollerad 2026-06-21.
Primär kärna
Rust
Rust-verifieraren och kärnan är en del av kontrollsidan.
Granskningsartefakt
.npcert
Kanoniska certifikatbyte är objektet som ska granskas.
Omkontrollpunkt
manuell granskning
Repository-status och paketsynlighet måste granskas före publicering.
Utforskare av förtroendegräns
Klicka igenom vad som är betrott och vad som inte är det.
Klicka på varje nod för att se vad den gör, vad den producerar och vilken kontroll som fortfarande krävs.
OBETRODD
KONTROLLERAD
Viktig gräns
NPA är för närvarande inte en praktisk ersättning för Lean eller Rocq. Den här sidan förklarar certifikatcentrerad forskningsdesign och garanterar inte felfria kommersiella system eller automatisk teoremlösning.
Certifikatkontroll / förklarande simulering
Följ flödet för certifikatkontroll.
Webbläsarinteraktionen förklarar granskningsflödet. Den kör inte NPA, Rust, WASM eller verkliga beviscertifikat.
CLI-exempel
npa package verify-certs --root . --checker reference --json
NPA / granskningsspår
REDO
- 01 Läs certifikatetkanoniska byte / format VÄNTA
- 02 Kontrollera certifikatets hashcertifikatets hash VÄNTA
- 03 Kontrollera med kärnankontroll av beroende bevis VÄNTA
- 04 Kontrollera igen med referenskontrollenkälloberoende utlåtande VÄNTA
- 05 Jämför axiomrapportenaxiomrapportens hash VÄNTA
Utlåtande
Förklaringen har inte körts ännu.Kör förklaringen för att visualisera stegen i ordning.
Bevisekosystem
Tydliggör roller i stället för att rangordna verktyg.
Lean och Rocq är mogna ekosystem för bevisassistenter. NPA visas här som ett certifikatcentrerat forsknings- och implementeringsprojekt, inte som en ersättningsrankning.
| Post | Lean | Rocq | NPA |
|---|---|---|---|
| Placering | Programspråk och bevisassistent med öppen källkod. | Interaktiv teorembevisare med lång forskningshistoria. | Forsknings- och implementeringsrepository för certifikatförst-kontroll. |
| Typisk användning | Matematik, programvaruverifiering och programmering. | Matematik, specifikationer, programverifiering och extraktion. | Forskning om beviscertifikat och oberoende kontroll. |
| Betoning | Utbyggbarhet, bibliotek och interaktiv bevisföring. | Uttryckskraft, mogna metoder och bibliotek. | Liten betrodd bas och kanoniska certifikat. |
| Hur sidan behandlar det | Referens för lärande, jämförelse och interoperabilitet. | Referens för lärande, jämförelse och formaliseringsmetoder. | Finite Fields forskningsprojekt. |
| Gräns | Specialistkunskap krävs fortfarande. | Specialistkunskap krävs fortfarande. | Inte avsett som praktisk ersättning för Lean eller Rocq i nuläget. |
Forskningsmetod
Gör 'det fungerade' till ett upprepbart kontrollförfarande.
Del av forskningsproceduren och reproducerbar kontroll.
Fråga
Definiera vad som ska kontrolleras: prestanda, korrekthet, kompatibilitet eller omfattning.
Antaganden
Skriv ned antaganden, undantag, axiom, dataluckor och bias före utvärdering.
Artefakt
Behåll källkod, certifikat, indata, körloggar och hashvärden.
Oberoende kontroll
Kontrollera resultat via en annan väg än genereringssidan.
Jämförelsetest
Lås hårdvara, versioner, tidsgränser, instansuppsättningar och slumpfrön.
Begränsningar
Publicera misslyckanden, fall som inte stöds, prestandagränser och nästa validering.
Reproducerbarhetsbyggare
Kontrollera vad en forskningspublicering fortfarande saknar.
Checklistan behandlas endast i webbläsaren. Den är inte ett certifieringsbetyg.
Beredskap
0%Nästa åtgärd
Definiera forskningsfrågan och framgångsvillkoret först.Innan artefaktformat bestäms ska det vara klart vad som ska jämföras eller kontrolleras.
Offentliga artefakter
Följ offentliga artefakter från en ingång.
Sidan undviker GitHub API-anrop vid körning. Repository-status är en granskad ögonblicksbild som måste kontrolleras före publicering.
4 artefakter
finitefield-org
npa
bevisverktygskedja med certifikat först
VERIFIERA
package verify-certs
finitefield-org
npa-std
standardiserat teorempaket
ROLL
Std.Logic / Nat / List
finitefield-org
npa-mathlib
formellt matematikbibliotek
ROLL
formella teorempaket
GitHub
finitefield-org
index över offentliga repositoryn
INDEX
alla offentliga repositoryn
Ingen offentlig artefakt matchar sökningen.
Publiceringspolicy
Offentliga repositoryn, forskningsanteckningar och benchmarkar bör ange kontrolldatum, mognad, reproduktionssteg och kända begränsningar. Stjärnor och commit-antal visas inte som signaler för forskningskvalitet.
Från labb till drift
Ta in forskningsdisciplin i designen av verksamhetssystem.
Alla kundsystem behöver inte teorembevisning. Det användbara är att avgöra vad som måste vara betrott, jämfört, kontrollerat, korrigerat och godkänt av människor.
Labbpraxis
Skilj generering, beräkning och slutlig kontroll åt i stället för att lita lika mycket på varje lager.
Behåll indata, utdata, certifikat, hashvärden och loggar som granskningsbara artefakter.
Lås data, versioner, kommandon och utvärderingskriterier innan resultat jämförs.
Publicera begränsningar, misslyckade fall och olösta punkter med samma tyngd som resultaten.
Kundsystem
Definiera vem som matar in, vem som granskar, vem som åsidosätter och vem som bekräftar resultatet.
Visa begränsningar, utvärderingspoäng, avvisade kandidater och olösta punkter.
Bevara ändringar i villkor, beräkningskörningar och historik över slutligt godkännande.
Gör automatiserade resultat möjliga att korrigera, avvisa och förklara för operatörer.
01
Skift och bemanning
Visa regelöverträdelser och uppfyllda önskemål separat.
02 FordonsruttningHåll ruttskäl, kapacitet, tidsfönster och undantag synliga.
03 ProduktionsplaneringFörklara oplanerat arbete, flaskhalsar och avvägningar vid omställning.
04 TilldelningsmatchningVisa kandidatskäl och alternativ före godkännande.
Forskningsanteckningar
Håll uppdateringshistorik och bevisning läsbara.
Alla kort är inte publicerade artiklar. Förberedda anteckningar markeras inte som publicerat arbete förrän de har datum, källor och reproduktionssteg.
NPA / Aktuellt
Varför certifikat bör stå i centrum
Forskningsanteckning med tydlig status, källor och reproduktionsväg.
Visa offentligt repositoryDesignanteckning / planerad
Gör optimeringsresultat förklarbara
En designanteckning om att visa mål, hårda begränsningar, mjuka önskemål och olösta tilldelningar i gränssnittet.
Visa relaterade demonstrationerJämförelsetest / planerad
Villkor för rättvis jämförelse av lösare
En planerad anteckning om instansuppsättningar, tidsgränser, optimalitetsgap, slumpfrön och hårdvara.
Visa publiceringskriterierPoster märkta 'Förbereds' är inte publicerade artiklar. Efter publicering får varje anteckning datum, källa, författare, reproduktionsväg och kända begränsningar.
FAQ
Gränser för forskning, bevisverktyg och affärsanvändning.
Dessa gränser görs tydliga innan forskningssidor förväxlas med produktionsgarantier.
Läs om företaget01 Är Matematiklabbet en tjänst för kontraktsutveckling?
Nej. Det är en plats för att publicera forskningshållning och artefakter. I kunddialoger skiljer vi mellan tillämpbara metoder, metoder som behöver mer validering och ämnen på forskningsstadiet.
02 Kan NPA ersätta Lean eller Rocq?
Nej. Dagens NPA är inte en praktisk ersättning för Lean eller Rocq. Det är ett forsknings- och implementeringsprojekt kring certifikat, oberoende kontroll och en liten betrodd bas.
03 Litar ni på AI-genererade bevis som de är?
Nej. AI, sökning och taktiker hjälper till att skapa kandidater. Vi fokuserar på om det slutliga certifikatet godtas av en kontroll som är oberoende av dessa genereringsvägar.
04 Tar formell verifiering bort alla fel?
Nej. Formella metoder kontrollerar specifika egenskaper mot en uttrycklig specifikation. Fel specifikationer, kod utanför omfattningen, drift och externa tjänster behöver fortfarande separat granskning.
05 Hänger detta ihop med arbete med verksamhetssystem?
Ja. Vi tillämpar oftast disciplinen stegvis: begränsningar, resultatskäl, beräkningshistorik, behörighetsgränser och kontroller för viktig verksamhetslogik.
Diskutera ett problem
Diskutera arbetet som ska lösas, inte bara forskningsämnet.
Börja med det nuvarande kalkylbladet, reglerna och de ställen där människor korrigerar besluten. Vi kan reda ut om matematisk modellering, regelautomatisering eller en prototyp bör komma först.
Källögonblicksbild / 2026-06-21
NPA-påståenden bygger på en ögonblicksbild av repositoryt finitefield-org/npa. Positioneringen av Lean och Rocq bygger på deras officiella webbplatser. Repository-status, senaste taggar och metodgranskningsformuleringar kontrollerades 2026-06-28.