01 / Raja
Pidä luotettu perusta pienenä
Älä aseta monimutkaisia generaattoreita tai tekoälyä luottamuksen keskelle. Tee pieni tarkistuspuoli näkyväksi.
Finite Field / Math Lab
Rakenna näyttöä oikeellisuudesta, ei vain nopeita tuloksia.
Math Lab näyttää, miten käsittelemme matemaattista mallinnusta, teoreemojen todistamista, formaalia verifiointia, toistettavuutta ja luotettua toteutusta liioittelematta näytön vahvuutta.
- Julkiset hankkeet
- NPA / STD / MATHLIB
- Ydinkieli
- Rust
- NPA-tilannekuva
- v0.1.1
Todistusauditointi / käsitteellinen näkymä
Vain luettavissa
01 kanoniset tavut / muoto OK
02 certificate_hash OK
03 riippuvaisten todistusten tarkistus OK
04 lähteestä riippumaton tulos OK
Luottamusraja näkyvissä
Tämä sivu ei väitä, että NPA olisi käytännön korvaaja Leanille tai Rocqille, eikä selainpohjainen simulaatio aja NPA:ta.
Lab-periaate
Julkaise tulosten lisäksi myös tarkistuksen rajat.
Päätelmä kuten "se toimi", "se oli nopea" tai "se todistettiin" ei riitä. Näytämme syötteet, oletukset, luotetut osat, riippumattomasti tarkistettavat artefaktit ja ratkaisemattomat kysymykset erikseen.
02 / Näyttö
Tee näytöstä artefakti
Jätä sertifikaatit, tiivisteet, oletuslistat, vertailuasetelmat ja lokit muotoon, jonka muut voivat tarkistaa.
03 / Toista
Suunnittele toistettavaksi
Kiinnitä työkaluketjut, syötedata, ajokomennot ja kriteerit, jotta tulos voidaan tarkistaa uudelleen.
04 / Rehellisyys
Älä liioittele tutkimuksen tilaa
Näytä käytännön menetelmät, kokeet ja tutkimus erillään. Aseta rajoitukset tulosten viereen.
MENETELMÄARVIO
Palvelumenetelmän luokka, joka vaatii vielä rajauksen, vastuut, asiakkaan näytön ja hyväksynnän ennen kuin sitä voidaan kuvata projektivalmiiksi.
KOKEELLINEN
Toimiva toteutus on olemassa, mutta mittakaava, yhteensopivuus, suorituskyky tai määrittely voivat vielä muuttua. Versio ja toistovaiheet tarvitaan.
TUTKIMUS
Suunnittelu, arviointi, todistus tai toteutus on kesken. Tämä ei tarkoita kaupallista saatavuutta tai valmistumista.
Tutkimusportfolio
Katso tutkimusta kypsyyden ja artefaktien mukaan.
Jokainen kortti näyttää kypsyyden, artefaktit, nykytilan ja seuraavan validoinnin. Haku ja suodattimet käyttävät vain selaimen tilaa.
8 näytetään
KOKEELLINEN
AVOIN LÄHDEKOODI
01
Nano Proof Auditor
Sertifikaatit ensin -todistustyökaluketju
Tutkimustyökaluketju, joka asettaa kanoniset todistussertifikaatit ja pienen tarkistusperustan riippuvaisten todistusten arvioinnin keskelle.
- Artefaktit
- lähde / määrittely / CI-mallit
- Nykytila
- v0.1.1 julkinen tilannekuva
- Seuraava validointi
- ulkoiset teoreemapaketit ja riippumaton tarkistus
KOKEELLINEN
AVOIN LÄHDEKOODI
02
NPA-standardikirjasto
Logic / Nat / List / Algebra
Uudelleenkäytettävien NPA-perusteiden standardi teoreemapakettien repositorio.
- Artefaktit
- lähde / todistuspaketit
- Nykytila
- julkinen erillinen repositorio
- Seuraava validointi
- paketin rajaus ja yhteensopivuus
TUTKIMUS
AVOIN LÄHDEKOODI
03
NPA Math Library
Formaalin matematiikan kirjasto
Kirjastosuunta matemaattisten teoreemojen tallentamiseen riippumattomasti tarkistettavina todistuspaketteina.
- Artefaktit
- lähde / todistuspaketit
- Nykytila
- kehitteillä oleva julkinen repositorio
- Seuraava validointi
- kirjastorakenne ja riippuvuuksien auditointi
MENETELMÄARVIO
MENETELMÄ
04
Rajoitteiset suunnittelumallit
Aikataulutus / reititys / yhteensovitus
Menetelmä ehdottomien rajoitteiden ja arviointimittareiden erottamiseen vuoro-, käynti-, reititys-, tuotanto- ja yhteensovitustyössä.
- Artefaktit
- malli / prototyyppi / selitysraportti
- Nykytila
- palvelumenetelmä; julkinen väite rajattu menetelmäarvioon
- Seuraava validointi
- asiakasnäyttö ja rajauksen hyväksyntä
TUTKIMUS
MITTAUS
05
Toistettava ratkaisijoiden arviointi
Vertailuasetelma ja näyttö
Ohjelma instanssijoukkojen, laitteiston, aikarajojen, satunnaissiementen ja raakalokien kiinnittämiseen ennen suorituskykyväitteitä.
- Artefaktit
- vertailuasetelmien rekisteri / raakalokit / raportti
- Nykytila
- tutkimusohjelman suunnittelu
- Seuraava validointi
- ensimmäinen julkinen vertailuaineisto
TUTKIMUS
FORMAALIT MENETELMÄT
06
Kriittisen liiketoimintalogiikan verifiointi
Liiketoimintajärjestelmien invariantit
Tutkimus maksujen, käyttöoikeuksien, varaston ja tilasiirtymien erottamisesta määrittelyiksi ja invarianteiksi.
- Artefaktit
- määrittely / invariantit / testi- tai todistusraportti
- Nykytila
- rajauksen selvitys
- Seuraava validointi
- yhden rajatun tuotantoa muistuttavan tapauksen valinta
KOKEELLINEN
OHJELMISTOTEKNIIKKA
07
Pienet luotetut komponentit Rustissa
Pienet luotetut komponentit
Toteutustyö, joka pitää luottamuksen kannalta kriittiset osat, kuten tarkistimet ja tiivisteet, riittävän pieninä tarkastaa.
- Artefaktit
- NPA-ydin / sertifikaattikirjasto / vertailutarkistin
- Nykytila
- julkinen toteutus NPA:ssa
- Seuraava validointi
- riippumattoman tarkistimen yhteensopivuus
TUTKIMUS
TEKOÄLY × TODISTUS
08
Tekoälyavustus ja riippumaton tarkistus
Tuota vapaasti, tarkista tiukasti
Tutkimussuunta, jossa tekoäly sijoitetaan ehdokkaiden tuottamiseen ja lopullinen näyttö tarkistetaan riippumattomasti.
- Artefaktit
- ehdokasgeneraattori / sertifikaatti / tarkistinraportti
- Nykytila
- tutkimussuunta, joka on linjassa NPA:n luottamusmallin kanssa
- Seuraava validointi
- mitattu kirjoittamisen työnkulku
Vastaavaa tutkimusaluetta ei löytynyt.
Kokeile toista hakusanaa tai palauta kypsyysfilteri kohtaan kaikki.
Nano Proof Auditor
Erota todistusten tuottaminen siitä, mihin luotamme.
NPA on sertifikaatit ensin -todistustyökaluketju riippuvaisille todistuksille. Käyttöliittymäkerrokset, taktiikat, teoreemahaku, liitännäiset, tekoäly, lähdetiedostot ja CI-tila voivat auttaa ehdokkaiden luonnissa, mutta ne eivät ole luotettua todistusnäyttöä.
KOKEELLINENAVOIN LÄHDEKOODIAPACHE-2.0
Nykyinen tilannekuva
v0.1.1
Julkiset tiedot tarkistettu 2026-06-21.
Ensisijainen ydin
Rust
Rust-verifioija ja ydin ovat osa tarkistuspuolta.
Auditointiartefakti
.npcert
Kanoniset sertifikaattitavut ovat tarkistettava kohde.
Uudelleentarkistuksen kohta
manuaalinen arvio
Repositorion tila ja paketin näkyvyys on tarkistettava ennen julkaisua.
Luottamusrajan tutkija
Napsauta läpi, mihin luotetaan ja mihin ei.
Napsauta kutakin solmua nähdäksesi, mitä se tekee, mitä se tuottaa ja mikä tarkistus on edelleen tarpeen.
EI LUOTETTU
TARKISTETTU
Tärkeä raja
NPA ei ole tällä hetkellä käytännön korvaaja Leanille tai Rocqille. Tämä sivu selittää sertifikaattikeskeistä tutkimusasetelmaa eikä takaa virheettömiä kaupallisia järjestelmiä tai automaattista teoreemojen ratkaisemista.
Sertifikaatin tarkistus / selittävä simulaatio
Koe sertifikaatin tarkistuspolku.
Selainvuorovaikutus selittää tarkistuspolun. Se ei aja NPA:ta, Rustia, WASMia tai oikeita todistusten sertifikaatteja.
CLI-esimerkki
npa package verify-certs --root . --checker reference --json
NPA / auditointijälki
VALMIS
- 01 Lue sertifikaattikanoniset tavut / muoto ODOTA
- 02 Tarkista sertifikaatin tiivistecertificate_hash ODOTA
- 03 Tarkista ytimelläriippuvaisten todistusten tarkistus ODOTA
- 04 Tarkista uudelleen vertailutarkistimellalähteestä riippumaton tulos ODOTA
- 05 Vertaa aksioomaraporttiaaksioomaraportin tiiviste ODOTA
Tulos
Selitystä ei ole vielä ajettu.Käynnistä selitys, jotta näet vaiheet järjestyksessä.
Todistustyökalujen ekosysteemi
Selvennä roolit työkalujen paremmuusjärjestyksen sijaan.
Lean ja Rocq ovat kypsiä todistusavustajien ekosysteemejä. NPA esitetään tässä sertifikaattikeskeisenä tutkimus- ja toteutushankkeena, ei korvaajien paremmuusjärjestyksenä.
| Kohde | Lean | Rocq | NPA |
|---|---|---|---|
| Asema | Avoimen lähdekoodin ohjelmointikieli ja todistusavustaja. | Interaktiivinen teoreemantodistin, jolla on pitkä tutkimushistoria. | Tutkimus- ja toteutusrepositorio sertifikaatit ensin -tarkistukseen. |
| Tyypillinen käyttö | Matematiikka, ohjelmistojen verifiointi ja ohjelmointi. | Matematiikka, määrittelyt, ohjelmien verifiointi ja ekstraktio. | Todistussertifikaattien ja riippumattoman tarkistuksen tutkimus. |
| Painotus | Laajennettavuus, kirjastot ja interaktiivinen todistaminen. | Ilmaisuvoima, kypsät menetelmät ja kirjastot. | Pieni luotettu perusta ja kanoniset sertifikaatit. |
| Tämän sivun näkökulma | Oppimisen, vertailun ja yhteentoimivuuden viitekohta. | Oppimisen, vertailun ja formalisointimenetelmien viitekohta. | Finite Fieldin tutkimushanke. |
| Raja | Erikoisosaamista tarvitaan edelleen. | Erikoisosaamista tarvitaan edelleen. | Ei tällä hetkellä tarkoitettu käytännön korvaajaksi Leanille tai Rocqille. |
Tutkimusmenetelmä
Muunna "se toimi" toistettavaksi tarkistusmenettelyksi.
Tulos vahvistuu, kun joku voi ajaa sen uudelleen, tarkastaa sen ja hylätä sen samoissa olosuhteissa.
Kysymys
Määritä, mitä tarkistetaan: suorituskyky, oikeellisuus, yhteensopivuus vai rajaus.
Oletukset
Kirjaa oletukset, poissulut, aksioomat, datan aukot ja vinoumat ennen arviointia.
Artefakti
Säilytä lähde, sertifikaatit, syötteet, suorituslokit ja tiivisteet.
Riippumaton tarkistus
Tarkista tulokset eri polkua pitkin kuin tuottamispuoli.
Vertailuasetelma
Kiinnitä laitteisto, versiot, aikarajat, instanssijoukot ja satunnaissiemenet.
Rajat
Julkaise epäonnistumiset, tukemattomat tapaukset, suorituskyvyn rajat ja seuraava validointi.
Toistettavuuden rakentaja
Tarkista, mitä tutkimusjulkaisusta vielä puuttuu.
Tarkistuslista käsitellään vain selaimessa. Se ei ole sertifiointipisteytys.
Valmius
0%Seuraava toimi
Määritä ensin tutkimuskysymys ja onnistumisehto.Ennen artefaktimuotojen päättämistä lukitse, mitä verrataan tai tarkistetaan.
Julkiset artefaktit
Seuraa julkisia artefakteja yhdestä sisäänkäynnistä.
Sivu välttää ajonaikaisia GitHub API -kutsuja. Repositorion tila on tarkistettu tilannekuva, joka on tarkistettava ennen julkaisua.
4 artefaktia
finitefield-org
npa
sertifikaatit ensin -todistustyökaluketju
TARKISTUS
package verify-certs
finitefield-org
npa-std
standarditeoreemojen paketti
ROOLI
Std.Logic / Nat / List
finitefield-org
npa-mathlib
formaalin matematiikan kirjasto
ROOLI
formaalit teoreemapaketit
GitHub
finitefield-org
julkisten repositorioiden hakemisto
HAKEMISTO
kaikki julkiset repositoriot
Mikään julkinen artefakti ei vastaa hakua.
Julkaisukäytäntö
Julkisissa repositorioissa, tutkimusmuistiinpanoissa ja vertailuasetelmissa pitäisi näkyä tarkistuspäivä, kypsyys, toistovaiheet ja tunnetut rajoitukset. Tähtiä ja commit-määriä ei näytetä tutkimuslaadun signaaleina.
Laboratoriosta käytännön toimintaan
Tuo tutkimuksen kurinalaisuus liiketoimintajärjestelmien suunnitteluun.
Kaikki asiakasjärjestelmät eivät tarvitse teoreemojen todistamista. Hyödyllistä on päättää, mihin pitää luottaa, mitä verrataan, mitä tarkistetaan, mitä korjataan ja mitä ihmiset hyväksyvät.
Laboratoriokäytäntö
Erota tuottaminen, laskenta ja lopullinen tarkistus sen sijaan, että luottaisit kaikkiin kerroksiin samalla tavalla.
Säilytä syötteet, tulokset, sertifikaatit, tiivisteet ja lokit tarkistettavina artefakteina.
Kiinnitä data, versiot, komennot ja arviointikriteerit ennen tulosten vertailua.
Julkaise rajoitteet, epäonnistuneet tapaukset ja ratkaisemattomat kohdat samalla painolla kuin tulokset.
Asiakasjärjestelmä
Määritä, kuka syöttää tiedot, kuka tarkistaa, kuka ohittaa ja kuka vahvistaa tuloksen.
Näytä rajoitteet, arviointipisteet, hylätyt ehdokkaat ja ratkaisemattomat kohdat.
Säilytä ehtojen muutokset, laskenta-ajot ja lopullinen hyväksyntähistoria.
Tee automaattisesta tuloksesta korjattava, hylättävä ja käyttäjille selitettävä.
01
Vuorot ja miehitys
Näytä sääntörikkomukset ja toiveiden toteutuminen erikseen.
02 AjoneuvoreititysPidä reittien perustelut, kapasiteetti, aikaikkunat ja poikkeukset näkyvissä.
03 TuotannonsuunnitteluSelitä aikatauluttamaton työ, pullonkaulat ja asetusten vaihtojen kompromissit.
04 Tehtävien yhteensovitusNäytä ehdokkaiden perustelut ja vaihtoehdot ennen hyväksyntää.
Tutkimusmuistiinpanot
Pidä päivityshistoria ja näyttö luettavina.
Kaikki kortit eivät ole julkaistuja artikkeleita. Valmisteilla olevia muistiinpanoja ei merkitä julkaistuiksi töiksi ennen kuin niillä on päivämäärät, lähteet ja toistovaiheet.
NPA / nykytila
Miksi sertifikaatit asetetaan keskelle
Miksi lopullisen näytön pitäisi olla standardoitu sertifikaatti, jonka pieni riippumaton polku tarkistaa.
Katso julkinen repositorioSuunnittelumuistio / suunnitteilla
Optimointitulosten tekeminen selitettäviksi
Suunnittelumuistiinpano tavoitteiden, ehdottomien rajoitteiden, joustavien toiveiden ja ratkaisemattomien tehtävien näyttämisestä käyttöliittymässä.
Katso liittyvät demotVertailuasetelma / suunnitteilla
Reilun ratkaisijavertailun ehdot
Suunniteltu muistiinpano instanssijoukoista, aikarajoista, optimaalisuusväleistä, satunnaissiemenistä ja laitteistosta.
Katso julkaisukriteerit"Valmisteilla"-kohteet eivät ole julkaistuja artikkeleita. Julkaisun jälkeen jokainen muistiinpano saa päivämäärän, lähteen, tekijän, toistopolun ja tunnetut rajoitukset.
UKK
Tutkimuksen, todistustyökalujen ja liiketoimintakäytön rajat.
Nämä kohdat tehdään näkyviksi ennen kuin tutkimussivuja erehdytään pitämään tuotantotakuina.
Lue yrityksestä01 Onko Math Lab sopimuskehityspalvelu?
Ei. Se on paikka tutkimusotteen ja artefaktien julkaisemiseen. Asiakaskeskusteluissa erotamme sovellettavat menetelmät, lisävalidointia vaativat menetelmät ja tutkimusvaiheen aiheet.
02 Voiko NPA korvata Leanin tai Rocqin?
Ei. Nykyinen NPA ei ole käytännön korvaaja Leanille tai Rocqille. Se on sertifikaatteihin, riippumattomaan tarkistukseen ja pieneen luotettuun perustaan keskittyvä tutkimus- ja toteutushanke.
03 Luotatteko tekoälyn tuottamiin todistuksiin sellaisenaan?
Ei sellaisenaan. Tekoäly, haku ja taktiikat auttavat ehdokkaiden tuottamisessa. Keskitymme siihen, hyväksyykö tuottamispoluista riippumaton tarkistin lopullisen sertifikaatin.
04 Poistaako formaali verifiointi kaikki virheet?
Ei. Formaaleilla menetelmillä tarkistetaan tiettyjä ominaisuuksia eksplisiittistä määrittelyä vasten. Väärät määrittelyt, rajauksen ulkopuolinen koodi, operointi ja ulkoiset palvelut vaativat edelleen erillisen tarkastelun.
05 Liittyykö tämä liiketoimintajärjestelmiin?
Kyllä. Sovellamme kurinalaisuutta yleensä vaiheittain: rajoitteisiin, tulosten perusteluihin, laskentahistoriaan, käyttöoikeusrajoihin ja tärkeän liiketoimintalogiikan tarkistuksiin.
Keskustele ongelmasta
Voit keskustella ratkaistavasta työstä, et vain tutkimusaiheesta.
Aloita nykyisestä laskentataulukosta, säännöistä ja kohdista, joissa ihmiset korjaavat päätöksiä. Voimme selvittää, pitäisikö ensin tehdä matemaattinen malli, sääntöautomaatio vai prototyyppi.
Lähdetilanne / 2026-06-21
NPA-väitteet perustuvat finitefield-org/npa-repositorion tilannekuvaan. Leanin ja Rocqin asemointi perustuu niiden virallisiin sivustoihin. Repositorion tila, uusimmat tagit ja menetelmäarvion sanamuodot tarkistettiin 2026-06-28.