01 / Confine
Mantieni piccola la base fidata
Non mettere generatori complessi o IA al centro della fiducia. Rendi esplicito il lato di controllo piccolo.
Finite Field / Math Lab
Costruisci evidenze di correttezza,non solo risultati rapidi.
Math Lab mostra come trattiamo modellazione matematica, dimostrazione di teoremi, verifica formale, riproducibilità e implementazione fidata senza esagerare la forza delle evidenze.
- Progetti pubblici
- NPA / STD / MATHLIB
- Linguaggio principale
- Rust
- Snapshot NPA
- v0.1.1
Audit delle prove / vista concettuale
Solo lettura
01 byte canonici / formato OK
02 hash del certificato OK
03 controllo della prova dipendente OK
04 verdetto senza sorgente OK
Confine di fiducia visibile
Questa pagina non afferma che NPA sia un sostituto pratico di Lean o Rocq, e la simulazione nel browser non esegue NPA.
Principio del Lab
Pubblica non solo i risultati, ma anche il confine del controllo.
Una conclusione come “ha funzionato”, “era veloce” o “è stato dimostrato” non basta. Mostriamo separatamente dati di ingresso, assunzioni, parti fidate, artefatti controllabili in modo indipendente e problemi irrisolti.
02 / Evidenza
Trasforma l'evidenza in un artefatto
Lascia certificati, hash, liste di assunzioni, condizioni di benchmark e log in una forma ispezionabile da altri.
03 / Riproduzione
Progetta per la riproducibilità
Fissa toolchain, dati di ingresso, comandi di esecuzione e criteri affinché il risultato possa essere ricontrollato.
04 / Onestà
Non esagerare lo stato della ricerca
Mostra separatamente metodi pratici, esperimenti e ricerca. Metti le limitazioni accanto ai risultati.
REVISIONE METODO
Categoria di metodo di servizio che richiede ancora ambito, responsabilità, evidenze del cliente e approvazione prima di essere descritta come pronta per un progetto.
SPERIMENTALE
Esiste un'implementazione funzionante, ma scala, compatibilità, prestazioni o specifiche possono ancora cambiare. Servono versione e passaggi di riproduzione.
RICERCA
Progettazione, valutazione, prova o implementazione sono in corso. Questo non implica disponibilità commerciale né completamento.
Portfolio di ricerca
Visualizza la ricerca per maturità e artefatti.
Ogni scheda mostra maturità, artefatti, stato attuale e prossima validazione. Ricerca e filtri usano solo lo stato nel browser.
8 mostrati
SPERIMENTALE
OPEN SOURCE
01
Nano Proof Auditor
Toolchain di prova centrata sui certificati
Toolchain di ricerca che mette al centro certificati di prova canonici e una piccola base di controllo per revisionare prove dipendenti.
- Artefatti
- sorgente / specifica / template CI
- Attuale
- snapshot pubblico v0.1.1
- Prossima validazione
- pacchetti di teoremi esterni e controllo indipendente
SPERIMENTALE
OPEN SOURCE
02
NPA Standard Library
Logic / Nat / List / Algebra
Repository di pacchetti di teoremi standard per fondazioni NPA riutilizzabili.
- Artefatti
- sorgente / pacchetti di prove
- Attuale
- repository pubblico separato
- Prossima validazione
- ambito dei pacchetti e compatibilità
RICERCA
OPEN SOURCE
03
NPA Math Library
Libreria di matematica formale
Direzione di libreria per conservare teoremi matematici come pacchetti di prove controllabili in modo indipendente.
- Artefatti
- sorgente / pacchetti di prove
- Attuale
- repository pubblico in sviluppo
- Prossima validazione
- struttura della libreria e audit delle dipendenze
REVISIONE METODO
METODO
04
Modelli di pianificazione con vincoli
Pianificazione / percorsi / assegnazione
Metodo per separare vincoli rigidi e metriche di valutazione in lavori di turni, visite, percorsi, produzione e assegnazione.
- Artefatti
- modello / prototipo / report esplicativo
- Attuale
- metodo di servizio; affermazione pubblica limitata alla revisione del metodo
- Prossima validazione
- evidenze del cliente e approvazione dell'ambito
RICERCA
MISURAZIONE
05
Valutazione riproducibile dei solver
Benchmark ed evidenze
Programma per fissare insiemi di istanze, hardware, limiti di tempo, semi casuali e log grezzi prima di fare affermazioni sulle prestazioni.
- Artefatti
- registro benchmark / log grezzi / report
- Attuale
- disegno del programma di ricerca
- Prossima validazione
- primo corpus pubblico di benchmark
RICERCA
METODI FORMALI
06
Verifica della logica aziendale critica
Invarianti per sistemi aziendali
Ricerca sulla separazione di tariffe, permessi, inventario e transizioni di stato in specifiche e invarianti.
- Artefatti
- specifica / invarianti / test o report di prova
- Attuale
- studio di ambito
- Prossima validazione
- selezione di un caso limitato simile alla produzione
SPERIMENTALE
INGEGNERIA
07
Piccoli componenti fidati in Rust
Piccoli componenti fidati
Lavoro di implementazione che mantiene componenti critici per la fiducia, come verificatori e hash, abbastanza piccoli da essere ispezionati.
- Artefatti
- kernel NPA / crate dei certificati / verificatore di riferimento
- Attuale
- implementazione pubblica in NPA
- Prossima validazione
- compatibilità del verificatore indipendente
RICERCA
IA × PROVA
08
Assistenza IA e controllo indipendente
Genera liberamente, verifica rigorosamente
Direzione di ricerca che colloca l'IA nella generazione dei candidati mentre l'evidenza finale viene controllata in modo indipendente.
- Artefatti
- generatore di candidati / certificato / report del verificatore
- Attuale
- direzione di ricerca coerente con il modello di fiducia NPA
- Prossima validazione
- flusso di authoring misurato
Nessuna area di ricerca corrispondente trovata.
Prova un'altra parola chiave o riporta il filtro di maturità su tutti.
Nano Proof Auditor
Separa la generazione della prova da ciò di cui ci fidiamo.
NPA è una toolchain di prova centrata sui certificati per prove dipendenti. Interfacce, tattiche, ricerca di teoremi, plugin, IA, file sorgente e stato CI possono aiutare a creare candidati, ma non sono l'evidenza di prova fidata.
SPERIMENTALEOPEN SOURCEAPACHE-2.0
Snapshot attuale
v0.1.1
Informazioni pubbliche controllate il 2026-06-21.
Core principale
Rust
Il verificatore e il kernel Rust fanno parte del lato di controllo.
Artefatto di audit
.npcert
I byte canonici del certificato sono l'oggetto da ispezionare.
Punto di ricontrollo
revisione manuale
Stato del repository e visibilità dei pacchetti devono essere rivisti prima della pubblicazione.
Esploratore del confine di fiducia
Esplora che cosa è fidato e che cosa non lo è.
Fai clic su ciascun nodo per vedere che cosa fa, che cosa produce e quale controllo resta necessario.
UNTRUSTED
CHECKED
Confine importante
NPA non è attualmente un sostituto pratico di Lean o Rocq. Questa pagina spiega un disegno di ricerca centrato sui certificati e non garantisce sistemi commerciali privi di bug né dimostrazione automatica dei teoremi.
Controllo certificato / simulazione esplicativa
Sperimenta il flusso di controllo dei certificati.
L'interazione nel browser spiega il flusso di ispezione. Non esegue NPA, Rust, WASM né certificati di prova reali.
Esempio CLI
npa package verify-certs --root . --checker reference --json
NPA / traccia di audit
PRONTO
- 01 Leggi il certificatobyte canonici / formato ATTESA
- 02 Controlla l'hash del certificatohash del certificato ATTESA
- 03 Controlla con il kernelcontrollo della prova dipendente ATTESA
- 04 Ricontrolla con il verificatore di riferimentoverdetto senza sorgente ATTESA
- 05 Confronta il report sugli assiomihash del report sugli assiomi ATTESA
Verdetto
La spiegazione non è ancora stata eseguita.Esegui la spiegazione per visualizzare i passaggi in ordine.
Ecosistema delle prove
Chiarire i ruoli invece di classificare gli strumenti.
Lean e Rocq sono ecosistemi maturi per assistenti alla dimostrazione. Qui NPA è presentato come progetto di ricerca e implementazione centrato sui certificati, non come classifica sostitutiva.
| Voce | Lean | Rocq | NPA |
|---|---|---|---|
| Posizione | Linguaggio di programmazione open source e assistente alla dimostrazione. | Dimostratore interattivo di teoremi con una lunga storia di ricerca. | Repository di ricerca e implementazione per il controllo basato prima sui certificati. |
| Uso tipico | Matematica, verifica del software e programmazione. | Matematica, specifiche, verifica di programmi ed estrazione. | Ricerca su certificati di prova e controllo indipendente. |
| Enfasi | Estensibilità, librerie e dimostrazione interattiva. | Espressività, metodi maturi e librerie. | Base fidata piccola e certificati canonici. |
| Come lo tratta questa pagina | Riferimento per apprendimento, confronto e interoperabilità. | Riferimento per apprendimento, confronto e metodi di formalizzazione. | Progetto di ricerca di Finite Field. |
| Confine | La conoscenza specialistica resta necessaria. | La conoscenza specialistica resta necessaria. | Al momento non è pensato come sostituto pratico di Lean o Rocq. |
Metodo di ricerca
Trasforma “ha funzionato” in una procedura di controllo ripetibile.
Un risultato diventa più solido quando qualcuno può rieseguirlo, ispezionarlo e respingerlo alle stesse condizioni.
Domanda
Definisci che cosa deve essere controllato: prestazioni, correttezza, compatibilità o ambito.
Assunzioni
Scrivi assunzioni, esclusioni, assiomi, lacune nei dati e bias prima della valutazione.
Artefatto
Conserva sorgenti, certificati, dati di ingresso, log di esecuzione e hash.
Controllo indipendente
Controlla i risultati attraverso un percorso diverso dal lato generazione.
Benchmark
Fissa hardware, versioni, limiti di tempo, insiemi di istanze e semi casuali.
Limiti
Pubblica fallimenti, casi non supportati, confini di prestazione e prossima validazione.
Costruttore di riproducibilità
Controlla che cosa manca ancora a una pubblicazione di ricerca.
La checklist viene elaborata solo nel browser. Non è un punteggio di certificazione.
Prontezza
0%Prossima azione
Definisci prima domanda di ricerca e condizione di successo.Prima di decidere i formati degli artefatti, fissa che cosa verrà confrontato o controllato.
Artefatti pubblici
Traccia gli artefatti pubblici da un unico ingresso.
La pagina evita chiamate runtime all'API GitHub. Lo stato dei repository è uno snapshot revisionato da controllare prima della pubblicazione.
4 artefatti
finitefield-org
npa
toolchain di prova centrata sui certificati
VERIFY
package verify-certs
finitefield-org
npa-std
pacchetto standard di teoremi
ROLE
Std.Logic / Nat / List
finitefield-org
npa-mathlib
libreria di matematica formale
ROLE
pacchetti di teoremi formali
GitHub
finitefield-org
indice dei repository pubblici
INDEX
tutti i repository pubblici
Nessun artefatto pubblico corrisponde alla ricerca.
Politica di pubblicazione
Repository pubblici, note di ricerca e benchmark dovrebbero riportare data di controllo, maturità, passaggi di riproduzione e limitazioni note. Stelle e conteggi dei commit non sono mostrati come segnali di qualità della ricerca.
Dal laboratorio alle operazioni
Porta la disciplina della ricerca nella progettazione dei sistemi aziendali.
Non tutti i sistemi cliente hanno bisogno di dimostrazione di teoremi. Il trasferimento utile consiste nel decidere che cosa deve essere fidato, confrontato, controllato, corretto e approvato dalle persone.
Pratica di laboratorio
Separa generazione, calcolo e controllo finale invece di fidarti allo stesso modo di ogni livello.
Conserva dati di ingresso, risultati, certificati, hash e log come artefatti revisionabili.
Fissa dati, versioni, comandi e criteri di valutazione prima di confrontare i risultati.
Pubblica vincoli, casi falliti e punti irrisolti con lo stesso peso dei risultati.
Sistema cliente
Definisci chi inserisce, chi revisiona, chi deroga e chi conferma il risultato.
Mostra vincoli, punteggi di valutazione, candidati respinti e punti irrisolti.
Conserva modifiche delle condizioni, esecuzioni del calcolo e cronologia dell'approvazione finale.
Rendi il risultato automatico correggibile, rifiutabile e spiegabile agli operatori.
01
Turni e organico
Mostra separatamente violazioni delle regole e soddisfazione delle preferenze.
02 Percorsi dei veicoliMantieni visibili motivi del percorso, capacità, fasce orarie ed eccezioni.
03 Pianificazione della produzioneSpiega lavori non pianificati, colli di bottiglia e compromessi di attrezzaggio.
04 Assegnazione e abbinamentoMostra motivi dei candidati e alternative prima dell'approvazione.
Note di ricerca
Mantieni leggibili cronologia degli aggiornamenti ed evidenze.
Non ogni scheda è un articolo pubblicato. Le note in preparazione non sono etichettate come lavori pubblicati finché non ricevono date, fonti e passaggi di riproduzione.
NPA / Attuale
Perché mettere i certificati al centro
Perché l'evidenza finale dovrebbe essere un certificato standardizzato controllato da un piccolo percorso indipendente.
Vedi repository pubblicoNota di progettazione / pianificata
Rendere spiegabili i risultati dell'ottimizzazione
Nota di progettazione su come esporre obiettivi, vincoli rigidi, preferenze flessibili e assegnazioni irrisolte nella UI.
Vedi demo correlateBenchmark / pianificato
Condizioni per confrontare equamente i solver
Nota pianificata su insiemi di istanze, limiti di tempo, gap di ottimalità, semi casuali e hardware.
Vedi criteri di pubblicazioneGli elementi “In preparazione” non sono articoli pubblicati. Dopo la pubblicazione, ogni nota riceve data, fonte, autore, percorso di riproduzione e limitazioni note.
FAQ
Confini tra ricerca, strumenti di prova e uso aziendale.
Questi punti sono esplicitati prima che le pagine di ricerca vengano scambiate per garanzie di produzione.
Leggi informazioni sull'azienda01 Math Lab è un servizio di sviluppo su contratto?
No. È un luogo per pubblicare l'atteggiamento di ricerca e gli artefatti. Nelle discussioni con i clienti separiamo metodi applicabili, metodi che richiedono più validazione e temi ancora di ricerca.
02 NPA può sostituire Lean o Rocq?
No. L'NPA attuale non è un sostituto pratico di Lean o Rocq. È un progetto di ricerca e implementazione su certificati, controllo indipendente e base fidata piccola.
03 Vi fidate delle prove generate dall'IA così come sono?
No. IA, ricerca e tattiche aiutano a generare candidati. Ci concentriamo sul fatto che il certificato finale sia accettato da un verificatore indipendente da quei percorsi di generazione.
04 La verifica formale elimina tutti i bug?
No. I metodi formali controllano proprietà specifiche rispetto a una specifica esplicita. Specifiche sbagliate, codice fuori ambito, operazioni e servizi esterni richiedono comunque una revisione separata.
05 Questo si collega al lavoro sui sistemi aziendali?
Sì. Di solito applichiamo la disciplina gradualmente: vincoli, motivi del risultato, cronologia dei calcoli, confini dei permessi e controlli sulla logica aziendale importante.
Discuti un problema
Puoi discutere il lavoro da risolvere, non solo il tema di ricerca.
Parti dal foglio di calcolo attuale, dalle regole e dai punti in cui le decisioni vengono corrette dalle persone. Possiamo chiarire se convenga iniziare da modellazione matematica, automazione di regole o prototipo.
Snapshot fonti / 2026-06-21
Le affermazioni su NPA si basano sullo snapshot del repository finitefield-org/npa. Il posizionamento di Lean e Rocq si basa sui loro siti ufficiali. Stato dei repository, tag più recenti e formulazioni di revisione del metodo sono stati controllati il 2026-06-28.