NPA / Pemeriksaan bukti yang mengutamakan sertifikat

NPA: tampilkan batas bukti sebelum memercayai hasil.

Halaman ini menyusun ulang bagian NPA dari Math Lab sebagai halaman bukti mandiri: status publik, model kepercayaan, alur bukti, daftar klaim, repositori, sumber, dan pernyataan eksplisit bahwa NPA bukan pengganti.

Periksa batas kepercayaan Buka repositori GitHub

Status publik: Repositori riset; Ditampilkan sebagai riset dan implementasi, bukan sebagai layanan jaminan produksi.
Pemeriksaan ulang publik: 2026-07-02 / NPA v0.2.0; Tag Git terbaru yang diperiksa: npa v0.2.0, npa-std v0.1.0, npa-mathlib v0.1.30.
Lisensi: Apache-2.0; Apache-2.0 diverifikasi untuk npa, npa-std, dan npa-mathlib pada 2026-07-02.

Pemeriksaan ulang publik: 2026-07-02. Tag Git terbaru repositori NPA adalah v0.2.0; npa-std adalah v0.1.0; npa-mathlib adalah v0.1.30. Pin README paket ditampilkan sebagai konteks khusus repositori dan tidak digabungkan menjadi satu klaim versi NPA.

Pratinjau halaman bukti NPA yang menampilkan pemeriksaan sertifikat dan inspeksi batas kepercayaan — Visual ini adalah pratinjau statis hasil pemeriksaan sertifikat dan penjelasan batas kepercayaan. Ini bukan jejak NPA langsung.

Status publik

Nyatakan apa yang publik, apa yang menjadi bukti, dan kapan diperiksa ulang.

Halaman ini membuat landasannya terlihat: cuplikan kebenaran lokal, sumber repositori publik, dan tanggal pembacaan ulang final sebelum peluncuran.

Status publik

Repositori riset dan implementasi

Repositori GitHub bersifat publik, tetapi halaman ini menjelaskan repositori riset dan implementasi, bukan layanan yang telah diterapkan.

Pemeriksaan ulang publik

2026-07-02

Pembacaan ulang sumber publik selesai pada 2026-07-02. Rekonstruksi sumber asli masih menggunakan cuplikan kebenaran lokal 2026-06-21.

Bukti

Sertifikat dan hash

Cuplikan sumber mencatat .npcert kanonis, certificate_hash, export_hash, axiom_report_hash, dan putusan pemeriksa.

Lisensi

Apache-2.0 terverifikasi

Apache-2.0 diverifikasi untuk npa, npa-std, dan npa-mathlib melalui metadata lisensi publik pada 2026-07-02.

Batas

NPA bukan pengganti praktis untuk Lean atau Rocq. Simulasi inspeksi terdistribusi dalam peramban tidak menjalankan NPA itu sendiri. Tag publik, lisensi, dan visibilitas repositori diperiksa pada 2026-07-02 untuk pembacaan ulang final sebelum publikasi.

Batas kepercayaan

Pindahkan hanya sertifikat kanonis melintasi batas bukti.

Batas ini bukan tentang alat mana yang tampak canggih. Batas ini menentukan artefak mana yang boleh menjadi bukti setelah pemeriksaan independen.

Parser, elaborator, taktik, otomasi, pencarian teorema, plugin, sistem AI, berkas sumber, berkas replay, indeks teorema, rencana publikasi, status CI, halaman rilis, dan metadata registri tetap berada di sisi kandidat yang tidak tepercaya.

Alur bukti / simulasi penjelasan

Tampilkan alur yang tepat dari byte sertifikat hingga bukti pemeriksaan.

Simulasi peramban tidak menjalankan NPA itu sendiri, Rust, WASM, atau sertifikat bukti nyata. Simulasi memvisualisasikan urutan pemeriksaan tanpa sumber yang harus dipenuhi artefak nyata.

Jalur bukti CLI

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

NPA / jejak audit SIAP

01 Format sertifikatbyte .npcert kanonis / sertifikat yang dapat diurai / pemeriksaan format TUNGGU
02 Hash sertifikatbyte sertifikat / certificate_hash / ringkasan hash deterministik TUNGGU
03 Putusan kernelsertifikat / terima atau tolak / laporan pemeriksa Rust TUNGGU
04 Pemeriksa acuansertifikat yang dipatok hash / terima atau tolak secara independen / laporan pemeriksa tanpa sumber TUNGGU
05 Laporan aksiomapaket yang diperiksa / axiom_report_hash / inventaris asumsi TUNGGU

Putusan

Alur penjelasan belum dijalankan.

Jalankan penjelasan untuk menandai jalur pemeriksaan tanpa sumber secara berurutan.

Daftar klaim

Pisahkan bukti, fakta yang peka waktu, dan klaim batas.

Halaman ini tidak bergantung pada teks riset yang longgar. Setiap pernyataan publik ditautkan ke cuplikan kebenaran lokal, sumber, dan tindakan publikasi.

Klaim	Pernyataan publik	Keadaan	Sumber	Tindakan sebelum publikasi
CL-001	NPA mengutamakan sertifikat: batas yang dapat diaudit adalah artefak .npcert kanonis dan jalur pemeriksaan di sekitarnya.	Klaim publik terverifikasi	S01 / 2026-07-02	Tinjau kembali saat README berubah.
CL-002	Pemeriksaan ulang publik pada 2026-07-02 menemukan bahwa git tag terbaru repositori NPA adalah v0.2.0. README paket terkait masih menampilkan pin khusus repositori, sehingga pernyataan versi tetap dibatasi per repositori.	Pemeriksaan ulang publik terverifikasi	S01 / S02 / 2026-07-02	Batasi pernyataan tag pada repositori terkait.
CL-003	Cuplikan kebenaran lokal mencatat pin rangkaian alat Rust 1.95.0; informasi ini tidak digunakan sebagai klaim pemasaran.	Terverifikasi, peka waktu	S01 / 2026-07-02	Periksa kembali jika versi rangkaian alat ditampilkan.
CL-004	NPA bukan pengganti praktis untuk Lean atau Rocq. Batas ini harus tetap terlihat di setiap perbandingan.	Klaim batas terverifikasi	S01 / S03 / S05 / 2026-07-02	Pertahankan penyangkalan ini.
CL-005	npa-std dan npa-mathlib adalah repositori paket teorema publik yang terpisah dalam organisasi finitefield-org.	Klaim publik terverifikasi	S01 / S02 / 2026-07-02	Periksa kembali visibilitas repositori jika publikasi tertunda atau repositori berubah.
CL-006	Repositori npa, npa-std, dan npa-mathlib masing-masing menampilkan lisensi Apache-2.0 melalui metadata lisensi publiknya.	Klaim publik terverifikasi	S01 / S02 / 2026-07-02	Periksa kembali lisensi saat rilis utama.

Repositori dan lisensi

Nyatakan kode, repositori paket, dan visibilitas organisasi secara jelas.

Tautan repositori menunjuk ke sumber publik, tetapi tidak menjamin bahwa halaman ini tersinkron dengan status GitHub terbaru.

4 repositori ditampilkan

finitefield-org

npa

Rangkaian alat bantuan dan verifikasi bukti yang mengutamakan sertifikat.

Lisensi: Apache-2.0 diverifikasi dari lisensi pada 2026-07-02.
Verifikasi: Tag Git terbaru: v0.2.0. Belum ada rilis GitHub terbaru yang dipublikasikan. Referensi rangkaian alat saat ini dalam README: NPA_GIT_TAG=v0.2.0.

eksperimentalRust / OCamlmengutamakan sertifikat

Buka repositori

finitefield-org

npa-std

Repositori paket teorema standar untuk sumber bukti NPA.

Lisensi: Apache-2.0 diverifikasi dari lisensi pada 2026-07-02.
Verifikasi: Tag Git dan rilis GitHub terbaru: v0.1.0. Versi metadata paket dalam README: 0.1.0; pin rangkaian alat paket: NPA_GIT_TAG=v0.1.1.

eksperimentalpaket teoremasumber bukti

Buka repositori

finitefield-org

npa-mathlib

Repositori riset untuk pustaka matematika formal.

Lisensi: Apache-2.0 diverifikasi dari lisensi pada 2026-07-02.
Verifikasi: Tag Git terbaru: v0.1.30. Rilis GitHub terbaru: v0.1.9. Versi metadata paket dalam README: 0.2.1; pin rangkaian alat paket: NPA_GIT_TAG=v0.1.1.

risetmatematika formalpustaka

Buka repositori

finitefield-org

Organisasi GitHub Finite Field

Snapshot publik organisasi untuk keluarga repositori Lab.

Lisensi: Lisensi berlaku sesuai repositori masing-masing
Verifikasi: npa, npa-std, dan npa-mathlib bersifat publik menurut pembacaan ulang API GitHub pada 2026-07-02.

indeks publikcuplikan visibilitassumber

Buka organisasi

Repositori GitHub adalah sumber status kode publik. Lisensi, tag saat ini, visibilitas publik, dan pernyataan rilis diperiksa pada 2026-07-02 sebagai pembacaan ulang final M10-T14.

Pengaman ekosistem pembuktian

Perjelas peran sebelum membandingkan alat pembuktian.

Ini adalah tabel peran, bukan peringkat. Lean dan Rocq tetap menjadi ekosistem acuan asisten pembuktian; NPA disajikan sebagai riset dan implementasi yang berpusat pada sertifikat.

Butir	Lean	Rocq	NPA
Posisi	Bahasa pemrograman sumber terbuka dan asisten pembuktian.	Pembukti teorema interaktif dengan sejarah riset yang panjang.	Repositori riset dan implementasi untuk pemeriksaan yang berpusat pada sertifikat.
Penggunaan umum	Matematika, verifikasi perangkat lunak, dan pemrograman.	Matematika, spesifikasi, verifikasi program, dan ekstraksi.	Riset mengenai sertifikat bukti, pemeriksaan independen, dan basis tepercaya yang kecil.
Batas bukti	Kernel tepercaya dan ekosistemnya sendiri menentukan batas pemeriksaan.	Kernel dan pengembangan terperiksanya sendiri menentukan batas pemeriksaan.	Artefak .npcert kanonis berpindah dari pembuatan ke pemeriksaan.
Cara halaman ini memandangnya	Acuan untuk pembelajaran, perbandingan, dan interoperabilitas.	Acuan untuk pembelajaran, perbandingan, dan metode formalisasi.	Proyek riset Finite Field, bukan janji produk.
Batas	Pengetahuan spesialis tetap diperlukan.	Pengetahuan spesialis tetap diperlukan.	Saat ini NPA bukan pengganti praktis untuk Lean atau Rocq.

Situs resmi Lean Situs resmi Rocq Prover GitHub NPA

Sumber

Publikasikan peta sumber di samping interpretasinya.

Sumber ditampilkan agar pembaca dapat membedakan klaim yang berasal dari repositori publik, situs resmi alat pembuktian, dan konteks perusahaan.

S01

finitefield-org/npa

Sumber utama untuk tujuan dan model kepercayaan NPA, pernyataan tag repositori saat ini v0.2.0, perintah, tata letak repositori, dan lisensi.

Buka sumber S02

Organisasi GitHub Finite Field

Sumber utama untuk visibilitas repositori publik, git tag terbaru, halaman rilis, dan cuplikan keluarga repositori Lab yang diperiksa pada 2026-07-02.

Buka sumber S03

Situs resmi Lean

Sumber utama untuk posisi publik Lean, diperiksa pada 2026-07-02.

Buka sumber S04

Referensi bahasa Lean

Sumber utama untuk teori tipe dependen dan konteks acuan kernel, diperiksa pada 2026-07-02.

Buka sumber S05

Situs resmi Rocq Prover

Sumber utama untuk posisi publik Rocq, diperiksa pada 2026-07-02.

Buka sumber S06

Situs perusahaan FINITE FIELD

Sumber perusahaan untuk merek Finite Field dan konteks bisnis.

Buka sumber

FAQ

Status NPA dan batas verifikasi.

Jawaban menekankan batas kepercayaan sebelum pembaca salah menganggap halaman riset sebagai layanan asisten pembuktian yang telah diterapkan.

Baca tentang perusahaan

01 Apakah halaman ini merupakan jaminan produk?

Tidak. NPA ditampilkan di sini sebagai repositori riset dan implementasi.

02 Bisakah NPA menggantikan Lean atau Rocq?

Tidak. NPA bukan pengganti praktis untuk Lean atau Rocq.

03 Apakah halaman menjalankan verifikasi NPA nyata?

Tidak. Simulasi peramban tidak menjalankan NPA itu sendiri, Rust, WASM, atau sertifikat bukti nyata.

04 Apa yang dianggap sebagai bukti di sini?

Artefak sertifikat, hash deterministik, hasil kernel/pemeriksa Rust, hasil pemeriksa acuan tanpa sumber, dan laporan aksioma membentuk bukti di sisi pemeriksaan.

05 Fakta mana yang perlu diperiksa ulang?

Versi publik saat ini, visibilitas repositori, pin rangkaian alat, teks lisensi, dan pernyataan sumber diperiksa ulang pada 2026-07-02.

Dari disiplin bukti ke operasi

Gunakan disiplin bukti yang sama ketika keputusan bisnis harus dapat dipercaya.

Untuk sistem bisnis, pelajaran yang berguna bukanlah menambahkan pembuktian teorema di mana-mana. Pelajarannya adalah memutuskan apa yang harus dibuat, diperiksa, dicatat, diperbaiki, dan disetujui manusia.

Periksa masalah bisnis Lihat prototipe