Δημόσια κατάσταση
Αποθετήριο έρευνας και υλοποίησης
Το αποθετήριο GitHub είναι δημόσιο, αλλά αυτή η σελίδα περιγράφει αποθετήριο έρευνας και υλοποίησης, όχι αναπτυγμένη υπηρεσία.
Επιστροφή στο Math Lab
NPA / Έλεγχος αποδείξεων με πρώτο το πιστοποιητικό
NPA: αποκαλύψτε το όριο των αποδεικτικών στοιχείων πριν εμπιστευτείτε ένα αποτέλεσμα.
Αυτή η σελίδα ανακατασκευάζει την ενότητα NPA του Math Lab ως ανεξάρτητη σελίδα τεκμηρίων: δημόσια κατάσταση, μοντέλο εμπιστοσύνης, ροή απόδειξης, μητρώο ισχυρισμών, αποθετήρια, πηγές και ρητή διατύπωση μη αντικατάστασης.
- Δημόσια κατάσταση
- Ερευνητικό αποθετήριο
- Παρουσιάζεται ως έρευνα και υλοποίηση, όχι ως υπηρεσία διασφάλισης παραγωγής.
- Δημόσιος επανέλεγχος
- 2026-07-02 / NPA v0.2.0
- Ελεγμένες πιο πρόσφατες ετικέτες git: npa v0.2.0, npa-std v0.1.0, npa-mathlib v0.1.30.
- Άδεια
- Apache-2.0
- Η Apache-2.0 επαληθεύτηκε για τα npa, npa-std και npa-mathlib στις 2026-07-02.
Δημόσιος επανέλεγχος: 2026-07-02. Η πιο πρόσφατη ετικέτα git του αποθετηρίου NPA είναι v0.2.0· το npa-std είναι v0.1.0· το npa-mathlib είναι v0.1.30. Οι δεσμεύσεις στα README παρουσιάζονται ως πλαίσιο ειδικό για κάθε αποθετήριο και δεν συγχωνεύονται σε έναν ισχυρισμό έκδοσης NPA.
Δημόσια κατάσταση
Δηλώστε τι είναι δημόσιο, τι αποτελεί αποδεικτικό στοιχείο και πότε επανελέγχθηκε.
Η σελίδα καθιστά ορατή τη βάση της: τοπικό στιγμιότυπο αναφοράς, δημόσια πηγή αποθετηρίου και ημερομηνία τελικού ελέγχου πριν από την έναρξη.
Δημόσιος επανέλεγχος
2026-07-02
Ο επανέλεγχος δημόσιων πηγών ολοκληρώθηκε στις 2026-07-02. Η αρχική ανακατασκευή εξακολουθεί να χρησιμοποιεί το τοπικό στιγμιότυπο αναφοράς της 2026-06-21.
Τεκμήρια
Πιστοποιητικά και αποτυπώματα
Το στιγμιότυπο πηγής καταγράφει canonical .npcert, certificate_hash, export_hash, axiom_report_hash και ετυμηγορίες ελεγκτών.
Άδεια
Apache-2.0 επαληθευμένη
Η Apache-2.0 επαληθεύτηκε για τα npa, npa-std και npa-mathlib μέσω δημόσιων μεταδεδομένων LICENSE στις 2026-07-02.
Όριο
Το NPA δεν αποτελεί πρακτική αντικατάσταση του Lean ή του Rocq. Η προσομοίωση επιθεώρησης στον περιηγητή δεν εκτελεί το ίδιο το NPA. Οι δημόσιες ετικέτες, η άδεια και η ορατότητα αποθετηρίων ελέγχθηκαν στις 2026-07-02 για τον τελικό επανέλεγχο δημοσίευσης.
Όριο εμπιστοσύνης
Περάστε μόνο ένα κανονικό πιστοποιητικό από το όριο αποδεικτικών στοιχείων.
Το όριο δεν αφορά ποιο εργαλείο φαίνεται εξελιγμένο. Αφορά ποιο τεκμήριο επιτρέπεται να γίνει αποδεικτικό στοιχείο μετά από ανεξάρτητο έλεγχο.
Ο αναλυτής, ο elaborator, οι τακτικές, η αυτοματοποίηση, η αναζήτηση θεωρημάτων, τα πρόσθετα, τα συστήματα AI, τα αρχεία πηγής, τα αρχεία επανάληψης, τα ευρετήρια θεωρημάτων, τα σχέδια δημοσίευσης, η κατάσταση CI, οι σελίδες εκδόσεων και τα μεταδεδομένα μητρώου παραμένουν στη μη έμπιστη πλευρά υποψηφίων.
Pipeline απόδειξης / επεξηγηματική προσομοίωση
Εμφανίστε την ακριβή ροή από τα byte του πιστοποιητικού έως τα τεκμήρια ελέγχου.
Η προσομοίωση του προγράμματος περιήγησης δεν εκτελεί το ίδιο το NPA, το Rust, το WASM ή πραγματικά πιστοποιητικά αποδείξεων. Οπτικοποιεί τη σειρά ελέγχου χωρίς πηγαίο κώδικα που πρέπει να ικανοποιούν τα πραγματικά τεκμήρια.
Διαδρομή τεκμηρίωσης CLI
npa package verify-certs --root . --checker reference --json
NPA / ίχνος ελέγχου
ΕΤΟΙΜΟ
- 01 Μορφή πιστοποιητικούκανονικά byte .npcert / αναγνώσιμο πιστοποιητικό / έλεγχος μορφής ΑΝΑΜΟΝΗ
- 02 Αποτύπωμα πιστοποιητικούbyte πιστοποιητικού / certificate_hash / ντετερμινιστικό αποτύπωμα ΑΝΑΜΟΝΗ
- 03 Απόφαση πυρήναπιστοποιητικό / αποδοχή ή απόρριψη / αναφορά ελεγκτή Rust ΑΝΑΜΟΝΗ
- 04 Ελεγκτής αναφοράςπιστοποιητικό με κλειδωμένο αποτύπωμα / ανεξάρτητη αποδοχή ή απόρριψη / αναφορά ελεγκτή χωρίς πηγαία εξάρτηση ΑΝΑΜΟΝΗ
- 05 Αναφορά αξιωμάτωνελεγμένο πακέτο / axiom_report_hash / κατάλογος παραδοχών ΑΝΑΜΟΝΗ
Αποτέλεσμα
Η επεξηγηματική ροή δεν έχει εκτελεστεί ακόμη.Εκτελέστε την εξήγηση για να επισημάνετε με τη σειρά τη διαδρομή ελέγχου χωρίς πηγαίο κώδικα.
Μητρώο ισχυρισμών
Διαχωρίστε τα αποδεικτικά στοιχεία, τα χρονικά ευαίσθητα δεδομένα και τους ισχυρισμούς ορίων.
Η σελίδα δεν βασίζεται σε αόριστο ερευνητικό κείμενο. Κάθε δημόσια δήλωση συνδέεται με τοπικό στιγμιότυπο αναφοράς, πηγή και ενέργεια πριν από τη δημοσίευση.
| Ισχυρισμός | Δημόσια διατύπωση | Κατάσταση | Πηγή | Ενέργεια πριν από τη δημοσίευση |
|---|---|---|---|---|
| CL-001 | Το NPA θέτει το πιστοποιητικό σε πρώτο πλάνο: το ελέγξιμο όριο είναι το κανονικό τεκμήριο .npcert και η διαδρομή ελέγχου γύρω του. | Επαληθευμένος δημόσιος ισχυρισμός | S01 / 2026-07-02 | Επανεξετάστε όταν αλλάξει το README. |
| CL-002 | Ο δημόσιος επανέλεγχος της 2026-07-02 διαπίστωσε ότι η πιο πρόσφατη ετικέτα git του αποθετηρίου NPA ήταν η v0.2.0. Τα README των σχετικών πακέτων εξακολουθούν να εμφανίζουν δεσμεύσεις ειδικές για κάθε αποθετήριο, επομένως η διατύπωση για τις εκδόσεις παραμένει περιορισμένη ανά αποθετήριο. | Επαληθευμένος δημόσιος επανέλεγχος | S01 / S02 / 2026-07-02 | Διατηρήστε τη διατύπωση της ετικέτας περιορισμένη στο αντίστοιχο αποθετήριο. |
| CL-003 | Το τοπικό στιγμιότυπο αναφοράς καταγράφει δέσμευση στην αλυσίδα εργαλείων Rust 1.95.0· δεν χρησιμοποιείται ως ισχυρισμός μάρκετινγκ. | Επαληθευμένο, χρονικά ευαίσθητο | S01 / 2026-07-02 | Επανελέγξτε αν εμφανίζεται η έκδοση της αλυσίδας εργαλείων. |
| CL-004 | Το NPA δεν αποτελεί πρακτική αντικατάσταση του Lean ή του Rocq. Αυτό το όριο πρέπει να παραμένει ορατό σε κάθε σύγκριση. | Επαληθευμένος ισχυρισμός ορίου | S01 / S03 / S05 / 2026-07-02 | Διατηρήστε την αποποίηση ευθύνης. |
| CL-005 | Τα npa-std και npa-mathlib είναι χωριστά δημόσια αποθετήρια πακέτων θεωρημάτων στον οργανισμό finitefield-org. | Επαληθευμένος δημόσιος ισχυρισμός | S01 / S02 / 2026-07-02 | Επανελέγξτε την ορατότητα των αποθετηρίων αν καθυστερήσει η δημοσίευση ή αλλάξουν τα αποθετήρια. |
| CL-006 | Τα αποθετήρια npa, npa-std και npa-mathlib δημοσιεύουν άδεια Apache-2.0 μέσω των δημόσιων μεταδεδομένων LICENSE. | Επαληθευμένος δημόσιος ισχυρισμός | S01 / S02 / 2026-07-02 | Επανελέγξτε το LICENSE σε μεγάλη έκδοση. |
Αποθετήρια και άδεια
Κάντε σαφή τον κώδικα, τα αποθετήρια πακέτων και την ορατότητα του οργανισμού.
Οι σύνδεσμοι αποθετηρίων δείχνουν σε δημόσιες πηγές, αλλά δεν εγγυώνται ότι η σελίδα είναι συγχρονισμένη με την πιο πρόσφατη κατάσταση του GitHub.
4 αποθετήρια εμφανίζονται
finitefield-org
npa
Αλυσίδα εργαλείων βοήθειας και επαλήθευσης αποδείξεων με επίκεντρο τα πιστοποιητικά.
- Άδεια
- Η Apache-2.0 επαληθεύτηκε από το LICENSE στις 2026-07-02.
- Επαλήθευση
- Πιο πρόσφατη ετικέτα git: v0.2.0. Δεν έχει δημοσιευτεί νεότερη έκδοση GitHub. Τρέχουσα αναφορά αλυσίδας εργαλείων στο README: NPA_GIT_TAG=v0.2.0.
πειραματικόRust / OCamlπρώτα το πιστοποιητικό
Άνοιγμα αποθετηρίου
finitefield-org
npa-std
Αποθετήριο τυπικού πακέτου θεωρημάτων για πηγές αποδείξεων NPA.
- Άδεια
- Η Apache-2.0 επαληθεύτηκε από το LICENSE στις 2026-07-02.
- Επαλήθευση
- Πιο πρόσφατη ετικέτα git και έκδοση GitHub: v0.1.0. Έκδοση μεταδεδομένων πακέτου στο README: 0.1.0· δέσμευση αλυσίδας εργαλείων πακέτου: NPA_GIT_TAG=v0.1.1.
πειραματικόπακέτο θεωρημάτωνπηγή απόδειξης
Άνοιγμα αποθετηρίου
finitefield-org
npa-mathlib
Ερευνητικό αποθετήριο βιβλιοθήκης τυπικών μαθηματικών.
- Άδεια
- Η Apache-2.0 επαληθεύτηκε από το LICENSE στις 2026-07-02.
- Επαλήθευση
- Πιο πρόσφατη ετικέτα git: v0.1.30. Πιο πρόσφατη έκδοση GitHub: v0.1.9. Έκδοση μεταδεδομένων πακέτου στο README: 0.2.1· δέσμευση αλυσίδας εργαλείων πακέτου: NPA_GIT_TAG=v0.1.1.
έρευνατυπικά μαθηματικάβιβλιοθήκη
Άνοιγμα αποθετηρίου
finitefield-org
Οργανισμός GitHub της Finite Field
Δημόσιο στιγμιότυπο οργανισμού για την οικογένεια αποθετηρίων Lab.
- Άδεια
- Ισχύουν άδειες ανά αποθετήριο
- Επαλήθευση
- Τα npa, npa-std και npa-mathlib είναι δημόσια σύμφωνα με τον επανέλεγχο API του GitHub στις 2026-07-02.
δημόσιο ευρετήριοστιγμιότυπο ορατότηταςπηγή
Άνοιγμα οργανισμού
Κανένα αποθετήριο δεν αντιστοιχεί στην τρέχουσα αναζήτηση.
Τα αποθετήρια GitHub είναι η πηγή για τη δημόσια κατάσταση του κώδικα. Η άδεια, οι τρέχουσες ετικέτες, η δημόσια ορατότητα και η διατύπωση εκδόσεων ελέγχθηκαν στις 2026-07-02 κατά τον τελικό επανέλεγχο M10-T14.
Πλαίσιο οικοσυστήματος αποδείξεων
Διευκρινίστε τους ρόλους πριν συγκρίνετε εργαλεία αποδείξεων.
Αυτός είναι πίνακας ρόλων, όχι κατάταξη. Τα Lean και Rocq παραμένουν οικοσυστήματα αναφοράς για βοηθούς αποδείξεων· το NPA παρουσιάζεται ως έρευνα και υλοποίηση με επίκεντρο τα πιστοποιητικά.
| Στοιχείο | Lean | Rocq | NPA |
|---|---|---|---|
| Θέση | Γλώσσα προγραμματισμού ανοικτού κώδικα και βοηθός αποδείξεων. | Διαδραστικό σύστημα απόδειξης θεωρημάτων με μακρά ερευνητική ιστορία. | Αποθετήριο έρευνας και υλοποίησης για έλεγχο με επίκεντρο τα πιστοποιητικά. |
| Τυπική χρήση | Μαθηματικά, επαλήθευση λογισμικού και προγραμματισμός. | Μαθηματικά, προδιαγραφές, επαλήθευση προγραμμάτων και εξαγωγή. | Έρευνα σε πιστοποιητικά αποδείξεων, ανεξάρτητο έλεγχο και μικρή έμπιστη βάση. |
| Όριο αποδεικτικών στοιχείων | Ο δικός του έμπιστος πυρήνας και το οικοσύστημα ορίζουν το όριο ελέγχου. | Ο δικός του πυρήνας και οι ελεγμένες αναπτύξεις ορίζουν το όριο ελέγχου. | Το κανονικό τεκμήριο .npcert περνά από την παραγωγή στον έλεγχο. |
| Πώς το αντιμετωπίζει η σελίδα | Αναφορά για μάθηση, σύγκριση και διαλειτουργικότητα. | Αναφορά για μάθηση, σύγκριση και μεθόδους τυποποίησης. | Ερευνητικό έργο της Finite Field, όχι υπόσχεση προϊόντος. |
| Όριο | Εξακολουθούν να απαιτούνται εξειδικευμένες γνώσεις. | Εξακολουθούν να απαιτούνται εξειδικευμένες γνώσεις. | Το NPA δεν αποτελεί προς το παρόν πρακτική αντικατάσταση του Lean ή του Rocq. |
Πηγές
Δημοσιεύστε τον χάρτη πηγών δίπλα στην ερμηνεία.
Οι πηγές εμφανίζονται ώστε ο αναγνώστης να διακρίνει ποιοι ισχυρισμοί προέρχονται από δημόσια αποθετήρια, επίσημους ιστοτόπους εργαλείων αποδείξεων και εταιρικό πλαίσιο.
S01
finitefield-org/npa
Κύρια πηγή για τον σκοπό και το μοντέλο εμπιστοσύνης του NPA, τη διατύπωση της τρέχουσας ετικέτας v0.2.0 του αποθετηρίου, τις εντολές, τη διάταξη αποθετηρίου και την άδεια.
Άνοιγμα πηγής S02Finite Field GitHub organization
Κύρια πηγή για τη δημόσια ορατότητα αποθετηρίων, τις πιο πρόσφατες ετικέτες git, τις σελίδες εκδόσεων και το στιγμιότυπο της οικογένειας Lab που ελέγχθηκε στις 2026-07-02.
Άνοιγμα πηγής S03Επίσημος ιστότοπος Lean
Κύρια πηγή για τη δημόσια τοποθέτηση του Lean, ελεγμένη στις 2026-07-02.
Άνοιγμα πηγής S04Αναφορά γλώσσας Lean
Κύρια πηγή για τη θεωρία εξαρτημένων τύπων και το πλαίσιο αναφοράς πυρήνα, ελεγμένη στις 2026-07-02.
Άνοιγμα πηγής S05Επίσημος ιστότοπος Rocq Prover
Κύρια πηγή για τη δημόσια τοποθέτηση του Rocq, ελεγμένη στις 2026-07-02.
Άνοιγμα πηγής S06Εταιρικός ιστότοπος FINITE FIELD
Εταιρική πηγή για το εμπορικό σήμα Finite Field και το επιχειρησιακό πλαίσιο.
Άνοιγμα πηγήςFAQ
Κατάσταση NPA και όρια επαλήθευσης.
Οι απαντήσεις τονίζουν το όριο εμπιστοσύνης πριν οι αναγνώστες συγχέουν μια ερευνητική σελίδα με αναπτυγμένη υπηρεσία βοηθού αποδείξεων.
Μάθετε για την εταιρεία01 Αποτελεί αυτή η σελίδα εγγύηση προϊόντος;
Όχι. Το NPA παρουσιάζεται εδώ ως αποθετήριο έρευνας και υλοποίησης.
02 Μπορεί το NPA να αντικαταστήσει το Lean ή το Rocq;
Όχι. Το NPA δεν αποτελεί πρακτική αντικατάσταση του Lean ή του Rocq.
03 Εκτελεί η σελίδα πραγματική επαλήθευση NPA;
Όχι. Η προσομοίωση του προγράμματος περιήγησης δεν εκτελεί το ίδιο το NPA, το Rust, το WASM ή πραγματικά πιστοποιητικά αποδείξεων.
04 Τι θεωρείται αποδεικτικό στοιχείο εδώ;
Το τεκμήριο πιστοποιητικού, τα ντετερμινιστικά αποτυπώματα, το αποτέλεσμα του πυρήνα/ελεγκτή Rust, το αποτέλεσμα του ελεγκτή αναφοράς χωρίς πηγαία εξάρτηση και η αναφορά αξιωμάτων αποτελούν τα τεκμήρια της πλευράς ελέγχου.
05 Ποια δεδομένα χρειάζονται επανέλεγχο;
Η τρέχουσα δημόσια έκδοση, η ορατότητα αποθετηρίων, οι δεσμεύσεις αλυσίδας εργαλείων, το κείμενο άδειας και η διατύπωση πηγών επανελέγχθηκαν στις 2026-07-02.
Από την πειθαρχία αποδείξεων στις λειτουργίες
Εφαρμόστε την ίδια πειθαρχία αποδεικτικών στοιχείων όταν μια επιχειρησιακή απόφαση πρέπει να είναι αξιόπιστη.
Για τα επιχειρησιακά συστήματα, το χρήσιμο δίδαγμα δεν είναι να προσθέσουμε απόδειξη θεωρημάτων παντού. Είναι να αποφασίσουμε τι πρέπει να παράγεται, να ελέγχεται, να καταγράφεται, να διορθώνεται και να εγκρίνεται από ανθρώπους.