Finite Field / Stærðfræðistofa

Byggðu sönnunargögn um réttmæti, ekki aðeins hraðar niðurstöður.

Stærðfræðistofan sýnir hvernig við vinnum með stærðfræðilega líkanagerð, setningasannanir, formlega sannprófun, endurtekningarhæfni og trausta útfærslu án þess að ýkja styrk sönnunargagna.

Skoða rannsóknarsvið Opna NPA-síðuna

Opinber verkefni: NPA / STD / MATHLIB
Kjarnamál: Rust
NPA útgáfa: v0.1.1

Sönnunarúttekt / hugtakayfirlit Aðeins til lestrar

01 stöðluð bætaraðir / snið Í LAGI

02 tætigildi vottorðs Í LAGI

03 athugun háðra sannana Í LAGI

04 frumkóðalaus úrskurður Í LAGI

Traustmörk eru sýnileg

Þessi síða heldur því ekki fram að NPA sé hagnýtur staðgengill Lean eða Rocq, og vafrahermunin keyrir ekki NPA.

Meginregla stofunnar

Birta ekki aðeins niðurstöður, heldur líka mörk athugunar.

Niðurstaða á borð við „það virkaði“, „það var hratt“ eða „það var sannað“ er ekki nóg. Við sýnum inntök, forsendur, trausta hluta, óháð athuganlega gripi og óleyst atriði sérstaklega.

01 / Mörk

Hafðu trausta grunninn lítinn

Settu ekki flókna rafla eða gervigreind í miðju traustsins. Gerðu litlu athugunarhliðina skýra.

02 / Sönnunargögn

Gerðu sönnunargögn að grip

Skildu eftir vottorð, tætigildi, forsendulista, viðmiðunarskilyrði og keyrsluskrár á formi sem aðrir geta skoðað.

03 / Endurkeyrsla

Hannaðu fyrir endurtekningarhæfni

Festu verkfærakeðjur, inntaksgögn, keyrsluskipanir og viðmið svo hægt sé að athuga niðurstöðuna aftur.

04 / Heiðarleiki

Ýktu ekki stöðu rannsókna

Sýndu hagnýtar aðferðir, tilraunir og rannsóknir aðskildar. Settu takmarkanir við hlið niðurstaðna.

AÐFERÐARRÝNI

Flokkur þjónustuaðferðar sem þarf enn umfang, ábyrgð, sönnunargögn frá viðskiptavini og samþykki áður en hægt er að lýsa henni sem verkefnishæfri.

TILRAUN

Virk útfærsla er til, en stærð, samhæfni, afköst eða forskrift geta enn breyst. Útgáfa og endurkeyrsluskref þurfa að fylgja.

RANNSÓKN

Hönnun, mat, sönnun eða útfærsla er í vinnslu. Þetta felur ekki í sér markaðsframboð eða lokið verk.

Rannsóknasafn

Skoðaðu rannsóknir eftir þroska og gripum.

Hvert spjald sýnir þroska, gripi, núverandi stöðu og næstu staðfestingu. Leit og síur nota aðeins stöðu í vafranum.

8 sýnd

TILRAUN OPINN KÓÐI

Nano Proof Auditor

Vottorðsmiðuð sönnunarverkfærakeðja

Rannsóknarverkfærakeðja sem setur stöðluð sönnunarvottorð og lítinn athugunargrunn í miðju rýni á háðum sönnunum.

Gripir: frumkóði / forskrift / CI-sniðmát
Núverandi: v0.1.1 opinber stöðumynd
Næsta staðfesting: ytri setningapakkar og óháð athugun

Opna NPA-upplýsingar

TILRAUN OPINN KÓÐI

NPA Standard Library

Logic / Nat / List / Algebra

Staðlað setningapakkasafn fyrir endurnýtanlega NPA-grunna.

Gripir: frumkóði / sönnunarpakkar
Núverandi: opinbert skipt gagnasafn
Næsta staðfesting: umfang pakka og samhæfni

GitHub

RANNSÓKN OPINN KÓÐI

NPA Math Library

Formlegt stærðfræðisafn

Safnstefna fyrir að geyma stærðfræðisetningar sem óháð athuganlega sönnunarpakka.

Gripir: frumkóði / sönnunarpakkar
Núverandi: opinbert gagnasafn í þróun
Næsta staðfesting: uppbygging safns og úttekt á háðum

GitHub

AÐFERÐARRÝNI AÐFERÐ

Skilyrt skipulagslíkön

Vaktir / leiðir / úthlutun

Aðferð til að aðgreina hörð skilyrði og matsmælikvarða í vöktum, heimsóknum, leiðum, framleiðslu og úthlutun.

Gripir: líkan / frumgerð / skýringarskýrsla
Núverandi: þjónustuaðferð; opinber fullyrðing takmörkuð við aðferðarrýni
Næsta staðfesting: sönnunargögn viðskiptavinar og samþykkt umfang

Skoða frumgerð

RANNSÓKN MÆLING

Endurtekningarhæft mat á leysurum

Viðmiðunarpróf og sönnunargögn

Áætlun um að festa tilvikasöfn, vélbúnað, tímamörk, slembifræ og hráar keyrsluskrár áður en fullyrt er um afköst.

Gripir: viðmiðunarprófaskrá / hráar skrár / skýrsla
Núverandi: hönnun rannsóknaráætlunar
Næsta staðfesting: fyrsta opinbera viðmiðunarprófasafn

Skoða aðferð

RANNSÓKN FORMLEGAR AÐFERÐIR

Sannprófun mikilvægrar viðskiptarökfræði

Óbreytur fyrir viðskiptakerfi

Rannsókn á því að aðgreina gjöld, heimildir, birgðir og stöðubreytingar í forskriftir og óbreytur.

Gripir: forskrift / óbreytur / prófa- eða sönnunarskýrsla
Núverandi: umfangsrannsókn
Næsta staðfesting: velja eitt afmarkað framleiðslulíkt tilvik

Skoða öryggishönnun

TILRAUN VERKFRÆÐI

Litlir traustir hlutar í Rust

Litlir traustir hlutar

Útfærsluvinna sem heldur traustmikilvægum hlutum eins og athugurum og tætigildum nógu litlum til að skoða.

Gripir: NPA-kjarni / vottorðskassi / viðmiðunarathugari
Núverandi: opinber útfærsla í NPA
Næsta staðfesting: samhæfni óháðs athugara

Skoða frumkóða

RANNSÓKN GERVIGREIND × SÖNNUN

Gervigreindaraðstoð og óháð athugun

Búa frjálst til, athuga strangt

Rannsóknarstefna þar sem gervigreind er notuð við gerð frambjóðenda en lokasönnunargögn eru athuguð óháð.

Gripir: frambjóðendarafall / vottorð / athugaraskýrsla
Núverandi: rannsóknarstefna í samræmi við traustlíkan NPA
Næsta staðfesting: mælt höfundarflæði

Skoða traustmörk

Ekkert rannsóknarsvið passaði.

Prófaðu annað leitarorð eða stilltu þroskasíuna aftur á allt.

Nano Proof Auditor

Aðgreindu gerð sannana frá því sem við treystum.

NPA er vottorðsmiðuð sönnunarverkfærakeðja fyrir háðar sannanir. Framendar, taktík, setningaleit, viðbætur, gervigreind, frumskrár og CI-staða geta hjálpað við að búa til frambjóðendur, en eru ekki traust sönnunargögn.

TILRAUNOPINN KÓÐIAPACHE-2.0

Núverandi útgáfa

v0.1.1

Opinberar upplýsingar yfirfarnar 2026-06-21.

Aðalkjarni

Rust

Rust-sannreynir og kjarni eru hluti af athugunarhliðinni.

Úttektargripur

.npcert

Staðlaðir vottorðsbætar eru hluturinn sem á að skoða.

Endurathugunarpunktur

handvirk rýni

Yfirfara þarf stöðu gagnasafns og sýnileika pakka fyrir birtingu.

Traustmarkaskoðari

Smelltu í gegnum hvað er treyst og hvað ekki.

Smelltu á hvern hnút til að skoða hvað hann gerir, hvað hann skilar og hvaða athugun er enn nauðsynleg.

ÓTRAUST

ATHUGAÐ

Mikilvæg mörk

NPA er ekki hagnýtur staðgengill Lean eða Rocq eins og staðan er nú. Þessi síða útskýrir vottorðsmiðaða rannsóknarhönnun og lofar hvorki villulausum viðskiptakerfum né sjálfvirkri setningasönnun.

Vottorðsathugun / skýringarhermun

Upplifðu flæði vottorðsathugunar.

Vafrasamskiptin útskýra skoðunarflæðið. Þau keyra ekki NPA, Rust, WASM eða raunveruleg sönnunarvottorð.

CLI-dæmi

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

NPA / úttektarslóð TILBÚIÐ

01 Lesa vottorðiðstöðluð bætaraðir / snið BÍÐ
02 Athuga tætigildi vottorðstætigildi vottorðs BÍÐ
03 Athuga með kjarnanumathugun háðra sannana BÍÐ
04 Endurathuga með viðmiðunarathugarafrumkóðalaus úrskurður BÍÐ
05 Bera saman frumsetningaskýrslutætigildi frumsetningaskýrslu BÍÐ

Úrskurður

Skýringin hefur ekki verið keyrð enn.

Keyrðu skýringuna til að sýna skrefin í réttri röð.

Sönnunarkerfi

Skýrðu hlutverk í stað þess að raða verkfærum.

Lean og Rocq eru þroskuð vistkerfi sönnunaraðstoðara. NPA er hér sýnt sem vottorðsmiðað rannsóknar- og útfærsluverkefni, ekki sem staðgengill eða stigagjöf.

Atriði	Lean	Rocq	NPA
Staða	Opið forritunarmál og sönnunaraðstoðari.	Gagnvirkur setningasannari með langa rannsóknarsögu.	Rannsóknar- og útfærslugagnasafn fyrir vottorðsmiðaða athugun.
Dæmigerð notkun	Stærðfræði, hugbúnaðarsannprófun og forritun.	Stærðfræði, forskriftir, forritasannprófun og útdráttur.	Rannsóknir á sönnunarvottorðum og óháðri athugun.
Áhersla	Útvíkkanleiki, söfn og gagnvirk sönnun.	Tjáningarmáttur, þroskaðar aðferðir og söfn.	Lítill traustur grunnur og stöðluð vottorð.
Hvernig þessi síða notar það	Viðmið fyrir nám, samanburð og samvirkni.	Viðmið fyrir nám, samanburð og formfestingaraðferðir.	Rannsóknarverkefni Finite Field.
Mörk	Sérfræðiþekking er enn nauðsynleg.	Sérfræðiþekking er enn nauðsynleg.	Ekki ætlað sem hagnýtur staðgengill Lean eða Rocq að svo stöddu.

Opinber vefsíða Lean Opinber vefsíða Rocq Prover NPA á GitHub

Rannsóknaraðferð

Breyttu „það virkaði“ í endurtekningarhæft athugunarferli.

Niðurstaða verður sterkari þegar einhver getur endurkeyrt hana, skoðað hana og hafnað henni við sömu skilyrði.

Spurning

Skilgreindu hvað á að athuga: afköst, réttmæti, samhæfni eða umfang.

Forsendur

Skráðu forsendur, útilokanir, frumsetningar, gagnagöt og bjaga fyrir mat.

Gripur

Geymdu frumkóða, vottorð, inntök, keyrsluskrár og tætigildi.

Óháð athugun

Athugaðu niðurstöður eftir annarri leið en þeirri sem bjó þær til.

Viðmiðunarpróf

Festu vélbúnað, útgáfur, tímamörk, tilvikasöfn og slembifræ.

Mörk

Birtu mistök, óstudd tilvik, afkastamörk og næstu staðfestingu.

Endurtekningarhæfnissmiður

Athugaðu hvað vantar enn í rannsóknarbirtingu.

Gátlistinn er aðeins unninn í vafranum. Hann er ekki vottunarstig.

Viðbúnaður

Rannsóknarspurning og árangursskilyrðiHvað telst árangur eða mistök. Fest verkfæri og háð atriðiÚtgáfur, læsingarskrár, vélbúnaður og umhverfi. Inntaksgögn eða gerðarferliNafnleynd, leyfi, uppruni og tætigildi. Endurkeyrsluröð skipanaFrá uppsetningu til niðurstöðu. Athuganlegir gripir og hráar skrárVottorð, skýrslur, keyrsluskrár og tætigildi. Mörk, mistök og opnar spurningarÓstudd tilvik og óleyst atriði.

Næsta aðgerð

Skilgreindu fyrst rannsóknarspurningu og árangursskilyrði.

Áður en gripasnið eru ákveðin þarf að festa hvað verður borið saman eða athugað.

Opinberir gripir

Fylgstu með opinberum gripum frá einum inngangi.

Síðan forðast GitHub API-köll í keyrslu. Staða gagnasafna er yfirfarin stöðumynd sem þarf að athuga fyrir birtingu.

4 gripir

finitefield-org

npa

vottorðsmiðuð sönnunarverkfærakeðja

Rust / OCamlApache-2.0Tilraun

STAÐFESTA package verify-certs

finitefield-org

npa-std

staðlaður setningapakki

SannanirPakkiTilraun

HLUTVERK Std.Logic / Nat / List

finitefield-org

npa-mathlib

formlegt stærðfræðisafn

StærðfræðiSannanirRannsókn

HLUTVERK formlegir setningapakkar

GitHub

finitefield-org

yfirlit yfir opinber gagnasöfn

StofnunOpinn kóði

YFIRLIT öll opinber gagnasöfn

Enginn opinber gripur passar við leitina.

Birtingarstefna

Opinber gagnasöfn, rannsóknarnótur og viðmiðunarpróf eiga að hafa yfirfarna dagsetningu, þroskastöðu, endurkeyrsluskref og þekktar takmarkanir. Stjörnur og commit-fjöldi eru ekki sýnd sem gæðamerki rannsókna.

Frá stofu til rekstrar

Flyttu rannsóknaraga inn í hönnun viðskiptakerfa.

Ekki hvert kerfi viðskiptavinar þarf setningasönnun. Gagnlegi flutningurinn er að ákveða hverju þarf að treysta, bera saman, athuga, leiðrétta og samþykkja af fólki.

Vinnulag stofunnar

Traustmörk

Aðgreindu gerð, útreikning og lokaathugun í stað þess að treysta öllum lögum jafnt.

Sönnunargögn

Haltu inntökum, úttökum, vottorðum, tætigildum og skrám sem yfirfarna gripi.

Endurtekningarhæfni

Festu gögn, útgáfur, skipanir og matsviðmið áður en niðurstöður eru bornar saman.

Mörk

Birtu skilyrði, misheppnuð tilvik og óleyst atriði með sama vægi og niðurstöður.

Kerfi viðskiptavinar

Umboð og ábyrgð

Skilgreindu hver skráir inn, hver rýnir, hver yfirskrifar og hver staðfestir niðurstöðuna.

Ástæður ákvarðana

Sýndu skilyrði, matsstig, hafnaða frambjóðendur og óleyst atriði.

Úttektarhæfni

Varðveittu breytingar á skilyrðum, reiknikeyrslur og sögu lokasamþykktar.

Mannlegt mat

Gerðu sjálfvirkar niðurstöður leiðréttanlegar, hafnanlegar og útskýranlegar fyrir notendur.

01 Vaktir og mönnun

Sýndu reglubrot og uppfyllingu óska sérstaklega.

02 Leiðagerð ökutækja

Hafðu leiðarástæður, afkastagetu, tímaglugga og undantekningar sýnileg.

03 Framleiðsluáætlun

Útskýrðu óáætluð verk, flöskuhálsa og skipti milli uppsetninga.

04 Úthlutun og pörun

Sýndu ástæður frambjóðenda og valkosti fyrir samþykki.

Rannsóknarnótur

Hafðu uppfærslusögu og sönnunargögn læsileg.

Ekki hvert spjald er birt grein. Nótur í undirbúningi eru ekki merktar sem birt verk fyrr en þær fá dagsetningar, heimildir og endurkeyrsluskref.

NPA / Núverandi2026.06.21

Af hverju setja vottorð í miðjuna

Af hverju lokasönnunargögn ættu að vera staðlað vottorð sem lítil óháð leið athugar.

Skoða opinbert gagnasafn

Hönnunarnóta / áætlaðÍ undirbúningi

Gera bestunarniðurstöður útskýranlegar

Hönnunarnóta um að sýna markmið, hörð skilyrði, mjúkar óskir og óleystar úthlutanir í viðmóti.

Skoða tengd sýnidæmi

Viðmiðunarpróf / áætlaðÍ undirbúningi

Skilyrði fyrir sanngjörnum samanburði leysara

Áætluð nóta um tilvikasöfn, tímamörk, bestunarbilið, slembifræ og vélbúnað.

Skoða birtingarviðmið

Atriði merkt „Í undirbúningi“ eru ekki birtar greinar. Eftir birtingu fær hver nóta dagsetningu, heimild, höfund, endurkeyrsluleið og þekktar takmarkanir.

Algengar spurningar

Rannsóknir, sönnunarverkfæri og mörk viðskiptanotkunar.

Þessi atriði eru gerð skýr áður en rannsóknarsíður eru ranglega túlkaðar sem framleiðsluábyrgðir.

Lesa um fyrirtækið

01 Er Stærðfræðistofan samningsbundin þróunarþjónusta?

Nei. Hún er staður til að birta rannsóknarviðhorf og gripi. Í samtölum við viðskiptavini aðgreinum við nothæfar aðferðir, aðferðir sem þurfa meiri staðfestingu og rannsóknarefni.

02 Getur NPA komið í stað Lean eða Rocq?

Nei. Núverandi NPA er ekki hagnýtur staðgengill Lean eða Rocq. Það er rannsóknar- og útfærsluverkefni um vottorð, óháða athugun og lítinn traustan grunn.

03 Treystið þið sönnunum sem gervigreind býr til óbreyttum?

Nei. Gervigreind, leit og taktík hjálpa til við að búa til frambjóðendur. Við horfum á hvort lokavottorðið sé samþykkt af athugara sem er óháður þeirri gerðarleið.

04 Fjarlægir formleg sannprófun allar villur?

Nei. Formlegar aðferðir athuga tiltekna eiginleika gagnvart skýrri forskrift. Rangar forskriftir, kóði utan umfangs, rekstur og ytri þjónusta þurfa áfram sérstaka rýni.

05 Tengist þetta vinnu við viðskiptakerfi?

Já. Við beitum yfirleitt aganum í áföngum: skilyrðum, ástæðum niðurstaðna, reiknisögu, heimildarmörkum og athugunum á mikilvægri viðskiptarökfræði.

Ræða vandamál

Þú getur rætt vinnuna sem á að leysa, ekki aðeins rannsóknarefnið.

Byrjaðu á núverandi töflureikni, reglum og stöðum þar sem fólk leiðréttir ákvarðanir. Við getum raðað því hvort stærðfræðileg líkanagerð, reglusjálfvirkni eða frumgerð eigi að koma fyrst.

Athuga rekstrarvandann Skoða frumgerð

Heimildastöðumynd / 2026-06-21

Fullyrðingar um NPA byggja á stöðumynd finitefield-org/npa gagnasafnsins. Staðsetning Lean og Rocq byggir á opinberum vefsíðum þeirra. Staða gagnasafna, nýjustu merki og orðalag aðferðarrýni voru yfirfarin 2026-06-28.