NPA / Zertifikatsorientierte Beweisprüfung
Diese Seite rekonstruiert den NPA-Abschnitt des Mathe-Labs als eigenständige Nachweisseite: öffentlicher Status, Vertrauensmodell, Beweispipeline, Aussagenregister, Repositorys, Quellen und eine ausdrückliche Nicht-Ersatz-Aussage.
Öffentliche Nachprüfung: 02.07.2026. Der neueste Git-Tag des NPA-Repositorys ist v0.2.0; npa-std ist v0.1.0; npa-mathlib ist v0.1.30. README-Bindungen der Pakete werden als repositoryspezifischer Kontext gezeigt und nicht zu einer einzigen NPA-Versionsangabe zusammengefasst.
Öffentlicher Status
Diese Seite macht ihre Grundlage sichtbar: einen lokalen Wahrheits-Snapshot, eine öffentliche Repositoryquelle und das Datum der abschließenden Vorab-Nachprüfung.
Das GitHub-Repository ist öffentlich, diese Seite beschreibt jedoch ein Forschungs- und Implementierungs-Repository und keinen bereitgestellten Dienst.
Die Nachprüfung der öffentlichen Quellen wurde am 02.07.2026 abgeschlossen. Die ursprüngliche Quellenrekonstruktion verwendet weiterhin den lokalen Wahrheits-Snapshot vom 21.06.2026.
Der Quellen-Snapshot erfasst kanonische .npcert-Dateien, certificate_hash, export_hash, axiom_report_hash und Prüferurteile.
Apache-2.0 wurde am 02.07.2026 für npa, npa-std und npa-mathlib anhand der öffentlichen LICENSE-Metadaten verifiziert.
Grenze
NPA ist kein praxistauglicher Ersatz für Lean oder Rocq. Die Browser-Simulation zur Prüfung führt NPA selbst nicht aus. Öffentliche Tags, Lizenz und Repository-Sichtbarkeit wurden am 02.07.2026 für die abschließende Veröffentlichungsnachprüfung geprüft.
Vertrauensgrenze
Die Grenze richtet sich nicht danach, welches Werkzeug anspruchsvoll wirkt. Entscheidend ist, welches Artefakt nach unabhängiger Prüfung als Nachweis gelten darf.
Parser, Elaborator, Taktiken, Automatisierung, Theoremsuche, Plugins, KI-Systeme, Quelldateien, Replay-Dateien, Theoremindizes, Veröffentlichungspläne, CI-Status, Release-Seiten und Registry-Metadaten bleiben auf der nicht vertrauenswürdigen Kandidatenseite.
Beweispipeline / Erklärungssimulation
Die Browser-Simulation führt weder NPA selbst noch Rust, WASM oder echte Beweiszertifikate aus. Sie visualisiert die quellfreie Prüfreihenfolge, die reale Artefakte erfüllen müssen.
CLI-Nachweispfad
npa package verify-certs --root . --checker reference --json
Urteil
Die erklärende Pipeline wurde noch nicht ausgeführt.Führen Sie die Erklärung aus, um den quellfreien Prüfpfad der Reihe nach zu markieren.
Aussagenregister
Die Seite stützt sich nicht auf unverbindliche Forschungstexte. Jede öffentliche Aussage ist mit einem lokalen Wahrheits-Snapshot, einer Quelle und einer Veröffentlichungsmaßnahme verknüpft.
| Behauptung | Öffentliche Formulierung | Status | Quelle | Maßnahme zur Veröffentlichung |
|---|---|---|---|---|
| CL-001 | NPA stellt das Zertifikat in den Mittelpunkt: Die prüfbare Grenze bilden das kanonische .npcert-Artefakt und der zugehörige Prüfpfad. | Verifizierte öffentliche Aussage | S01 / 2026-07-02 | Bei Änderungen an der README erneut prüfen. |
| CL-002 | Bei der öffentlichen Nachprüfung am 02.07.2026 war v0.2.0 der neueste Git-Tag des NPA-Repositorys. Die READMEs der zugehörigen Pakete nennen weiterhin repositoryspezifische Bindungen; Versionsangaben bleiben daher auf das jeweilige Repository beschränkt. | Verifizierte öffentliche Nachprüfung | S01 / S02 / 2026-07-02 | Tag-Angaben auf das jeweilige Repository beschränken. |
| CL-003 | Der lokale Wahrheits-Snapshot enthält eine Toolchain-Bindung an Rust 1.95.0; sie wird nicht als Marketingaussage verwendet. | Verifiziert, zeitabhängig | S01 / 2026-07-02 | Erneut prüfen, falls die Toolchain-Version angezeigt wird. |
| CL-004 | NPA ist kein praxistauglicher Ersatz für Lean oder Rocq. Diese Grenze muss bei jedem Vergleich sichtbar bleiben. | Verifizierte Grenzaussage | S01 / S03 / S05 / 2026-07-02 | Den Haftungsausschluss beibehalten. |
| CL-005 | npa-std und npa-mathlib sind getrennte öffentliche Repositorys für Theorempakete in der Organisation finitefield-org. | Verifizierte öffentliche Aussage | S01 / S02 / 2026-07-02 | Die Sichtbarkeit der Repositorys erneut prüfen, wenn sich die Veröffentlichung verzögert oder Repositorys geändert werden. |
| CL-006 | Die Repositorys npa, npa-std und npa-mathlib weisen über ihre öffentlichen LICENSE-Metadaten jeweils die Lizenz Apache-2.0 aus. | Verifizierte öffentliche Aussage | S01 / S02 / 2026-07-02 | LICENSE bei einer Hauptversion erneut prüfen. |
Repositorys und Lizenz
Repository-Links sind Verweise auf öffentliche Quellen, keine Garantie, dass diese Seite mit dem neuesten GitHub-Stand synchronisiert ist.
4 Repositorys angezeigt
finitefield-org
Zertifikatsorientierte Beweisunterstützung und Verifikations-Toolchain.
finitefield-org
Repository des Standard-Theorempakets für NPA-Beweisquellen.
finitefield-org
Forschungs-Repository für eine Bibliothek formaler Mathematik.
finitefield-org
Öffentlicher Snapshot der Organisation für die Lab-Repositoryfamilie.
Die GitHub-Repositorys sind die Quelle für den öffentlichen Codestatus. Lizenz, aktuelle Tags, öffentliche Sichtbarkeit und Release-Formulierungen wurden am 02.07.2026 als abschließende M10-T14-Nachprüfung geprüft.
Schutzrahmen für das Beweiswerkzeug-Ökosystem
Dies ist eine Rollentabelle, keine Rangliste. Lean und Rocq bleiben die Referenz-Ökosysteme für Beweisassistenten; NPA wird als zertifikatsorientierte Forschungs- und Implementierungsarbeit dargestellt.
| Element | Lean | Rocq | NPA |
|---|---|---|---|
| Einordnung | Quelloffene Programmiersprache und Beweisassistent. | Interaktiver Theorembeweiser mit langer Forschungsgeschichte. | Forschungs- und Implementierungs-Repository für zertifikatsorientierte Prüfung. |
| Typische Verwendung | Mathematik, Softwareverifikation und Programmierung. | Mathematik, Spezifikationen, Programmverifikation und Extraktion. | Forschung zu Beweiszertifikaten, unabhängiger Prüfung und einer kleinen vertrauenswürdigen Basis. |
| Nachweisgrenze | Der eigene vertrauenswürdige Kernel und das Ökosystem definieren die Prüfgrenze. | Der eigene Kernel und geprüfte Entwicklungen definieren die Prüfgrenze. | Das kanonische .npcert-Artefakt wechselt von der Erzeugung in die Prüfung. |
| Einordnung auf dieser Seite | Referenz für Lernen, Vergleich und Interoperabilität. | Referenz für Lernen, Vergleich und Formalisierungsmethoden. | Forschungsprojekt von Finite Field, kein Produktversprechen. |
| Grenze | Fachkenntnisse sind weiterhin erforderlich. | Fachkenntnisse sind weiterhin erforderlich. | NPA ist derzeit kein praxistauglicher Ersatz für Lean oder Rocq. |
Quellen
Die Quellen werden gezeigt, damit Leser erkennen können, welche Aussagen aus öffentlichen Repositorys, offiziellen Websites der Beweiswerkzeuge und dem Unternehmenskontext stammen.
Primärquelle für Zweck, Vertrauensmodell, Formulierung des aktuellen Repository-Tags v0.2.0, Befehle, Repositorystruktur und Lizenz von NPA.
Quelle öffnen S02Primärquelle für öffentliche Repository-Sichtbarkeit, neueste Git-Tags, Release-Seiten und den am 02.07.2026 geprüften Snapshot der Lab-Repositoryfamilie.
Quelle öffnen S03Primärquelle für die öffentliche Einordnung von Lean, geprüft am 02.07.2026.
Quelle öffnen S04Primärquelle für abhängige Typentheorie und Kernel-Referenzkontext, geprüft am 02.07.2026.
Quelle öffnen S05Primärquelle für die öffentliche Einordnung von Rocq, geprüft am 02.07.2026.
Quelle öffnen S06Unternehmensquelle für Marke und Geschäftskontext von Finite Field.
Quelle öffnenFAQ
Die Antworten betonen zuerst die Vertrauensgrenze, damit Leser eine Forschungsseite nicht mit einem bereitgestellten Beweisassistenten-Dienst verwechseln.
Mehr über das Unternehmen lesenVon Beweisdisziplin zu Betriebsabläufen
Für Geschäftssysteme besteht die nützliche Lehre nicht darin, überall Theorembeweise einzubauen. Entscheidend ist, festzulegen, was erzeugt, geprüft, protokolliert, korrigiert und von Menschen genehmigt werden muss.