01 / Limite
Garder la base de confiance petite
Ne placez pas les générateurs complexes ni l’IA au centre de la confiance. Rendez explicite le petit côté vérification.
Finite Field / Math Lab
Construire des preuves d’exactitude,pas seulement des résultats rapides.
Math Lab montre comment nous traitons la modélisation mathématique, la démonstration de théorèmes, la vérification formelle, la reproductibilité et les implémentations fiables sans surestimer les preuves.
- Projets publics
- NPA / STD / MATHLIB
- Langage central
- Rust
- Instantané NPA
- v0.1.1
Audit de preuve / vue conceptuelle
Lecture seule
01 octets canoniques / format OK
02 certificate_hash OK
03 vérification de preuve dépendante OK
04 verdict sans source OK
La limite de confiance est visible
Cette page ne prétend pas que NPA remplace Lean ou Rocq dans un usage pratique, et la simulation du navigateur n’exécute pas NPA.
Principe du laboratoire
Publier non seulement les résultats, mais aussi les limites de la vérification.
Une conclusion comme « ça a marché », « c’était rapide » ou « c’était prouvé » ne suffit pas. Nous montrons séparément les entrées, les hypothèses, les parties fiables, les artefacts vérifiables indépendamment et les problèmes non résolus.
02 / Preuve
Faire de la preuve un artefact
Laisser les certificats, hachages, listes d’hypothèses, conditions de benchmark et journaux dans une forme inspectable par d’autres.
03 / Reproduire
Concevoir pour la reproductibilité
Figer les chaînes d’outils, les données d’entrée, les commandes d’exécution et les critères afin que le résultat puisse être vérifié à nouveau.
04 / Clarté
Ne pas surestimer le statut de recherche
Présenter séparément les méthodes pratiques, les expériences et la recherche. Placer les limites à côté des résultats.
REVUE DE MÉTHODE
Catégorie de méthode de service qui exige encore un périmètre, des responsabilités, des preuves côté client et une approbation avant d’être décrite comme prête pour un projet.
EXPÉRIMENTAL
Une implémentation fonctionnelle existe, mais des changements d’échelle, de compatibilité, de performance ou de spécification restent possibles. La version et les étapes de reproduction sont nécessaires.
RECHERCHE
La conception, l’évaluation, la preuve ou l’implémentation est en cours. Cela ne signifie pas une disponibilité commerciale ni un achèvement.
Portefeuille de recherche
Voir la recherche par maturité et par artefacts.
Chaque carte indique la maturité, les artefacts, l’état actuel et la prochaine validation. La recherche et les filtres restent uniquement côté navigateur.
8 affichés
EXPÉRIMENTAL
CODE OUVERT
01
Nano Proof Auditor
Chaîne d’outils de preuve centrée sur les certificats
Chaîne d’outils de recherche qui place les certificats de preuve canoniques et une petite base de vérification au centre de l’examen des preuves dépendantes.
- Artefacts
- source / spécification / modèles CI
- Actuel
- instantané public v0.1.1
- Prochaine validation
- paquets de théorèmes externes et vérification indépendante
EXPÉRIMENTAL
CODE OUVERT
02
Bibliothèque standard NPA
Logique / Nat / List / Algebra
Dépôt de paquets de théorèmes standard pour les fondations réutilisables de NPA.
- Artefacts
- source / paquets de preuves
- Actuel
- dépôt public séparé
- Prochaine validation
- périmètre du paquet et compatibilité
RECHERCHE
CODE OUVERT
03
Bibliothèque mathématique NPA
Bibliothèque de mathématiques formelles
Orientation de bibliothèque pour stocker des théorèmes mathématiques sous forme de paquets de preuves vérifiables indépendamment.
- Artefacts
- source / paquets de preuves
- Actuel
- dépôt public en développement
- Prochaine validation
- structure de bibliothèque et audit des dépendances
REVUE DE MÉTHODE
MÉTHODE
04
Modèles de planification sous contraintes
Planification / Tournées / Affectation
Méthode pour séparer contraintes dures et indicateurs d’évaluation dans les postes, visites, tournées, productions et travaux d’affectation.
- Artefacts
- modèle / prototype / rapport explicatif
- Actuel
- méthode de service ; revendication publique limitée à la revue de méthode
- Prochaine validation
- preuves client et approbation du périmètre
RECHERCHE
MESURE
05
Évaluation reproductible des solveurs
Benchmark et preuves
Programme visant à fixer les jeux d’instances, le matériel, les limites de temps, les graines aléatoires et les journaux bruts avant toute revendication de performance.
- Artefacts
- registre de benchmark / journaux bruts / rapport
- Actuel
- conception du programme de recherche
- Prochaine validation
- premier corpus public de benchmarks
RECHERCHE
MÉTHODES FORMELLES
06
Vérification de la logique métier critique
Invariants pour les systèmes métier
Recherche sur la séparation des frais, autorisations, stocks et transitions d’état en spécifications et invariants.
- Artefacts
- spécification / invariants / rapport de test ou de preuve
- Actuel
- étude de périmètre
- Prochaine validation
- sélection d’un cas borné proche de la production
EXPÉRIMENTAL
INGÉNIERIE
07
Petits composants de confiance en Rust
Petits composants de confiance
Travail d’implémentation qui garde les pièces critiques pour la confiance, comme les vérificateurs et les hachages, assez petites pour être inspectées.
- Artefacts
- noyau NPA / crate de certificat / vérificateur de référence
- Actuel
- implémentation publique dans NPA
- Prochaine validation
- compatibilité du vérificateur indépendant
RECHERCHE
IA × PREUVE
08
Assistance par IA et vérification indépendante
Générer librement, vérifier strictement
Orientation de recherche qui place l’IA du côté de la génération de candidats, tandis que la preuve finale est vérifiée indépendamment.
- Artefacts
- générateur de candidats / certificat / rapport du vérificateur
- Actuel
- orientation de recherche cohérente avec le modèle de confiance NPA
- Prochaine validation
- flux de rédaction mesuré
Aucun axe de recherche correspondant n’a été trouvé.
Essayez un autre mot-clé ou remettez le filtre de maturité sur tous.
Nano Proof Auditor
Séparer la génération de preuves de ce à quoi nous faisons confiance.
NPA est une chaîne d’outils de preuve privilégiant les certificats pour les preuves dépendantes. Les interfaces, tactiques, recherches de théorèmes, plugins, l’IA, les fichiers source et l’état CI peuvent aider à créer des candidats, mais ils ne constituent pas la preuve fiable.
EXPÉRIMENTALCODE OUVERTAPACHE-2.0
Instantané actuel
v0.1.1
Informations publiques vérifiées le 2026-06-21.
Cœur principal
Rust
Le vérificateur et le noyau Rust font partie du côté vérification.
Artefact d’audit
.npcert
Les octets canoniques du certificat sont l’objet à inspecter.
Point de revérification
revue manuelle
L’état du dépôt et la visibilité du paquet doivent être revus avant publication.
Explorateur des limites de confiance
Parcourir ce qui est fiable et ce qui ne l’est pas.
Cliquez sur chaque nœud pour voir ce qu’il fait, ce qu’il produit et quel contrôle reste nécessaire.
NON FIABLE
VÉRIFIÉ
Limite importante
NPA ne remplace pas actuellement Lean ou Rocq dans un usage pratique. Cette page explique une conception de recherche centrée sur les certificats et ne garantit ni des systèmes commerciaux sans bugs, ni la résolution automatique de théorèmes.
Contrôle de certificat / simulation explicative
Parcourir le flux de vérification des certificats.
L’interaction dans le navigateur explique le flux d’inspection. Elle n’exécute ni NPA, ni Rust, ni WASM, ni de véritables certificats de preuve.
Exemple de CLI
npa package verify-certs --root . --checker reference --json
NPA / trace d’audit
PRÊT
- 01 Lire le certificatoctets canoniques / format ATTENTE
- 02 Vérifier le hachage du certificatcertificate_hash ATTENTE
- 03 Contrôler avec le noyauvérification de preuve dépendante ATTENTE
- 04 Revérifier avec le vérificateur de référenceverdict sans source ATTENTE
- 05 Comparer le rapport d’axiomeshachage du rapport d’axiomes ATTENTE
Verdict
L’explication n’a pas encore été lancée.Lancez l’explication pour visualiser les étapes dans l’ordre.
Écosystème de preuve
Clarifier les rôles au lieu de classer les outils.
Lean et Rocq sont des écosystèmes mûrs d’assistants de preuve. NPA est présenté ici comme un projet de recherche et d’implémentation centré sur les certificats, et non comme un classement de remplacement.
| Élément | Lean | Rocq | NPA |
|---|---|---|---|
| Position | Langage de programmation et assistant de preuve open source. | Démonstrateur interactif de théorèmes avec une longue histoire de recherche. | Dépôt de recherche et d’implémentation pour la vérification centrée sur les certificats. |
| Usage typique | Mathématiques, vérification logicielle et programmation. | Mathématiques, spécifications, vérification de programmes et extraction. | Recherche sur les certificats de preuve et la vérification indépendante. |
| Mise en avant | Extensibilité, bibliothèques et preuve interactive. | Expressivité, méthodes mûres et bibliothèques. | Petite base de confiance et certificats canoniques. |
| Traitement sur cette page | Référence pour l’apprentissage, la comparaison et l’interopérabilité. | Référence pour l’apprentissage, la comparaison et les méthodes de formalisation. | Projet de recherche Finite Field. |
| Limite | Des connaissances spécialisées restent nécessaires. | Des connaissances spécialisées restent nécessaires. | N’est pas destiné à remplacer Lean ou Rocq dans un usage pratique à ce stade. |
Méthode de recherche
Transformer « ça a marché » en procédure de vérification répétable.
Un résultat devient plus solide lorsqu’une autre personne peut le relancer, l’inspecter et le rejeter dans les mêmes conditions.
Question
Définir ce qui doit être vérifié : performance, exactitude, compatibilité ou périmètre.
Hypothèses
Écrire les hypothèses, exclusions, axiomes, lacunes de données et biais avant l’évaluation.
Artefact
Conserver la source, les certificats, les entrées, les journaux d’exécution et les hachages.
Contrôle indépendant
Contrôler les résultats par un chemin différent du côté génération.
Benchmark
Figer le matériel, les versions, les limites de temps, les jeux d’instances et les graines aléatoires.
Limites
Publier les échecs, les cas non pris en charge, les limites de performance et la prochaine validation.
Constructeur de reproductibilité
Vérifier ce qui manque encore à une publication de recherche.
La liste de contrôle est traitée uniquement dans le navigateur. Ce n’est pas une note de certification.
Préparation
0%Prochaine action
Définissez d’abord la question de recherche et la condition de réussite.Avant de décider des formats d’artefacts, fixez ce qui sera comparé ou vérifié.
Artefacts publics
Suivre les artefacts publics depuis une entrée unique.
La page évite les appels GitHub API à l’exécution. L’état des dépôts est un instantané revu qui doit être contrôlé avant publication.
4 artefacts
finitefield-org
npa
chaîne d’outils de preuve centrée sur les certificats
VERIFY
package verify-certs
finitefield-org
npa-std
paquet de théorèmes standard
ROLE
Std.Logic / Nat / List
finitefield-org
npa-mathlib
bibliothèque de mathématiques formelles
ROLE
paquets de théorèmes formels
GitHub
finitefield-org
index des dépôts publics
INDEX
tous les dépôts publics
Aucun artefact public ne correspond à la recherche.
Politique de publication
Les dépôts publics, notes de recherche et benchmarks doivent indiquer la date de vérification, la maturité, les étapes de reproduction et les limites connues. Les étoiles et le nombre de commits ne sont pas utilisés comme signaux de qualité de recherche.
Du laboratoire aux opérations
Appliquer la discipline de la recherche à la conception des systèmes métier.
Tous les systèmes clients n’ont pas besoin de démonstration de théorèmes. Le transfert utile consiste à déterminer ce qui doit être accepté, comparé, vérifié, corrigé et approuvé par des personnes.
Pratique du laboratoire
Séparer la génération, le calcul et la vérification finale au lieu d’accorder la même confiance à toutes les couches.
Conserver les entrées, sorties, certificats, hachages et journaux comme artefacts vérifiables.
Figer les données, les versions, les commandes et les critères d’évaluation avant de comparer les résultats.
Publier les contraintes, les cas d’échec et les points non résolus avec le même poids que les résultats.
Système client
Définir qui saisit les données, qui vérifie, qui passe outre et qui confirme le résultat.
Afficher les contraintes, les scores d’évaluation, les candidats rejetés et les points non résolus.
Conserver l’historique des changements de conditions, des calculs exécutés et de l’approbation finale.
Rendre les sorties automatisées corrigibles, rejetables et explicables aux opérateurs.
01
Postes et effectifs
Afficher séparément les violations de règles et la satisfaction des préférences.
02 Tournées de véhiculesGarder visibles les raisons de l’itinéraire, la capacité, les créneaux horaires et les exceptions.
03 Ordonnancement de productionExpliquer le travail non planifié, les goulets d’étranglement et les compromis de réglage.
04 Appariement des affectationsAfficher les raisons des candidats et les alternatives avant approbation.
Notes de recherche
Rendre l’historique des mises à jour et les preuves lisibles.
Toutes les cartes ne sont pas des articles publiés. Les notes en préparation ne sont pas présentées comme des travaux publiés tant qu’elles n’ont pas reçu de dates, de sources et d’étapes de reproduction.
NPA / actuel
Pourquoi placer les certificats au centre
Pourquoi la preuve finale devrait être un certificat standardisé vérifié par un petit chemin indépendant.
Voir le dépôt publicNote de conception / prévue
Rendre les résultats d’optimisation explicables
Note de conception sur l’affichage des objectifs, des contraintes dures, des préférences souples et des affectations non résolues dans l’interface.
Voir les démos associéesBenchmark / prévu
Conditions d’une comparaison équitable des solveurs
Note prévue sur les jeux d’instances, les limites de temps, les écarts d’optimalité, les graines aléatoires et le matériel.
Voir les critères de publicationLes éléments « Préparation » ne sont pas des articles publiés. Après publication, chaque note reçoit une date, une source, un auteur, un chemin de reproduction et des limites connues.
FAQ
Limites entre recherche, outils de preuve et usage métier.
Ces points sont explicités pour éviter de confondre les pages de recherche avec des garanties de production.
En savoir plus sur l’entreprise01 Math Lab est-il un service de développement contractuel ?
Non. C’est un espace pour publier une démarche de recherche et des artefacts. Dans les échanges avec les clients, nous séparons les méthodes applicables, celles qui nécessitent davantage de validation et les sujets encore au stade de la recherche.
02 NPA peut-il remplacer Lean ou Rocq ?
Non. Le NPA actuel ne remplace pas Lean ou Rocq dans un usage pratique. C’est un projet de recherche et d’implémentation autour des certificats, de la vérification indépendante et d’une petite base de confiance.
03 Faites-vous confiance telles quelles aux preuves générées par l’IA ?
Non. L’IA, la recherche et les tactiques aident à générer des candidats. Nous vérifions surtout si le certificat final est accepté par un vérificateur indépendant de ces chemins de génération.
04 La vérification formelle élimine-t-elle tous les bugs ?
Non. Les méthodes formelles vérifient des propriétés précises par rapport à une spécification explicite. Les spécifications erronées, le code hors périmètre, les opérations et les services externes nécessitent toujours un examen séparé.
05 Cela concerne-t-il les systèmes métier ?
Oui. Nous appliquons généralement cette discipline progressivement : contraintes, raisons des résultats, historique de calcul, limites d’autorisation et contrôles de la logique métier importante.
Discuter d’un problème
Vous pouvez discuter du travail à résoudre, et pas seulement du sujet de recherche.
À partir de la feuille de calcul actuelle, des règles et des endroits où les personnes corrigent les décisions, nous pouvons déterminer si la modélisation mathématique, l’automatisation des règles ou un prototype doit venir en premier.
Instantané des sources / 2026-06-21
Les affirmations sur NPA reposent sur l’instantané du dépôt finitefield-org/npa. Le positionnement de Lean et Rocq repose sur leurs sites officiels. L’état du dépôt, les dernières étiquettes et la formulation de revue de méthode ont été vérifiés le 2026-06-28.