Finite Field / Math Lab

Bangun bukti kebenaran,bukan hanya hasil cepat.

Math Lab adalah tempat kami menunjukkan cara menangani pemodelan matematis, pembuktian teorema, verifikasi formal, reproduksibilitas, dan implementasi tepercaya tanpa melebih-lebihkan bukti.

Lihat area riset Buka halaman NPA

Proyek publik: NPA / STD / MATHLIB
Bahasa inti: Rust
Cuplikan NPA: v0.1.1

Audit bukti / tampilan konseptual Hanya baca

01 byte kanonis / format OK

02 certificate_hash OK

03 pemeriksaan bukti dependen OK

04 putusan tanpa sumber OK

Batas kepercayaan terlihat

Halaman ini tidak mengklaim bahwa NPA adalah pengganti praktis untuk Lean atau Rocq, dan simulasi peramban tidak menjalankan NPA.

Prinsip Lab

Publikasikan bukan hanya hasil, tetapi juga batas pemeriksaan.

Kesimpulan seperti “berhasil”, “cepat”, atau “terbukti” belum cukup. Kami menampilkan masukan, asumsi, bagian tepercaya, artefak yang dapat diperiksa independen, dan masalah yang belum selesai secara terpisah.

01 / Batas

Jaga basis tepercaya tetap kecil

Jangan menempatkan generator kompleks atau AI di pusat kepercayaan. Buat sisi pemeriksaan yang kecil terlihat jelas.

02 / Bukti

Jadikan bukti sebagai artefak

Tinggalkan sertifikat, hash, daftar asumsi, kondisi tolok ukur, dan log dalam bentuk yang dapat diperiksa orang lain.

03 / Reproduksi

Rancang untuk reproduksibilitas

Tetapkan rangkaian alat, data masukan, perintah eksekusi, dan kriteria agar hasil dapat diperiksa kembali.

04 / Kejujuran

Jangan melebih-lebihkan status riset

Tampilkan metode praktis, eksperimen, dan riset secara terpisah. Letakkan batasan di samping hasil.

TINJAUAN METODE

Kategori metode layanan yang masih memerlukan cakupan, tanggung jawab, bukti klien, dan persetujuan sebelum disebut siap proyek.

EKSPERIMENTAL

Implementasi berjalan sudah ada, tetapi skala, kompatibilitas, kinerja, atau perubahan spesifikasi masih mungkin terjadi. Versi dan langkah reproduksi diperlukan.

RISET

Desain, evaluasi, bukti, atau implementasi sedang berlangsung. Ini tidak berarti tersedia secara komersial atau sudah selesai.

Portofolio riset

Lihat riset berdasarkan kematangan dan artefak.

Setiap kartu menampilkan kematangan, artefak, status saat ini, dan validasi berikutnya. Pencarian dan filter hanya memakai status di sisi peramban.

8 ditampilkan

EKSPERIMENTAL SUMBER TERBUKA

Nano Proof Auditor

Rangkaian alat pembuktian yang mengutamakan sertifikat

Rangkaian alat riset yang menempatkan sertifikat bukti kanonis dan basis pemeriksaan kecil di pusat tinjauan bukti dependen.

Artefak: sumber / spesifikasi / templat CI
Saat ini: cuplikan publik v0.1.1
Validasi berikutnya: paket teorema eksternal dan pemeriksaan independen

Buka detail NPA

EKSPERIMENTAL SUMBER TERBUKA

Pustaka Standar NPA

Logika / Nat / List / Aljabar

Repositori paket teorema standar untuk fondasi NPA yang dapat digunakan ulang.

Artefak: sumber / paket bukti
Saat ini: repositori publik terpisah
Validasi berikutnya: cakupan paket dan kompatibilitas

GitHub

RISET SUMBER TERBUKA

Pustaka Matematika NPA

Pustaka matematika formal

Arah pustaka untuk menyimpan teorema matematika sebagai paket bukti yang dapat diperiksa independen.

Artefak: sumber / paket bukti
Saat ini: repositori publik dalam pengembangan
Validasi berikutnya: struktur pustaka dan audit dependensi

GitHub

TINJAUAN METODE METODE

Model perencanaan berkendala

Penjadwalan / Rute / Penugasan

Metode untuk memisahkan kendala keras dan metrik evaluasi dalam pekerjaan shift, kunjungan, rute, produksi, dan penugasan.

Artefak: model / prototipe / laporan penjelasan
Saat ini: metode layanan; klaim publik dibatasi pada tinjauan metode
Validasi berikutnya: bukti klien dan persetujuan cakupan

Lihat prototipe

RISET PENGUKURAN

Evaluasi pemecah yang dapat direproduksi

Tolok ukur dan bukti

Program untuk menetapkan kumpulan instans, perangkat keras, batas waktu, benih acak, dan log mentah sebelum membuat klaim kinerja.

Artefak: registri tolok ukur / log mentah / laporan
Saat ini: desain program riset
Validasi berikutnya: korpus tolok ukur publik pertama

Lihat metode

RISET METODE FORMAL

Verifikasi untuk logika bisnis kritis

Invarian untuk sistem bisnis

Riset tentang memisahkan biaya, izin, persediaan, dan transisi status ke dalam spesifikasi dan invarian.

Artefak: spesifikasi / invarian / laporan uji atau bukti
Saat ini: studi cakupan
Validasi berikutnya: pilih satu kasus terbatas yang mirip produksi

Lihat desain keamanan

EKSPERIMENTAL REKAYASA

Komponen tepercaya kecil di Rust

Komponen tepercaya kecil

Pekerjaan implementasi yang menjaga bagian kritis kepercayaan seperti pemeriksa dan hash tetap cukup kecil untuk diperiksa.

Artefak: kernel NPA / paket sertifikat / pemeriksa acuan
Saat ini: implementasi publik di NPA
Validasi berikutnya: kompatibilitas pemeriksa independen

Lihat sumber

RISET AI × BUKTI

Bantuan AI dan pemeriksaan independen

Buat bebas, verifikasi ketat

Arah riset yang menempatkan AI pada pembuatan kandidat, sementara bukti akhir diperiksa secara independen.

Artefak: generator kandidat / sertifikat / laporan pemeriksa
Saat ini: arah riset yang konsisten dengan model kepercayaan NPA
Validasi berikutnya: alur penulisan yang terukur

Lihat batas kepercayaan

Tidak ada area riset yang cocok.

Coba kata kunci lain atau kembalikan filter kematangan ke semua.

Nano Proof Auditor

Pisahkan pembuatan bukti dari hal yang kita percaya.

NPA adalah rangkaian alat pembuktian yang mengutamakan sertifikat untuk bukti dependen. Antarmuka depan, taktik, pencarian teorema, plugin, AI, berkas sumber, dan status CI dapat membantu membuat kandidat, tetapi bukan bukti tepercaya.

EKSPERIMENTALSUMBER TERBUKAAPACHE-2.0

Cuplikan saat ini

v0.1.1

Informasi publik diperiksa pada 2026-06-21.

Inti utama

Rust

Pemeriksa dan kernel Rust adalah bagian dari sisi pemeriksaan.

Artefak audit

.npcert

Byte sertifikat kanonis adalah objek yang diperiksa.

Titik pemeriksaan ulang

tinjauan manual

Status repositori dan visibilitas paket harus ditinjau sebelum publikasi.

Penjelajah batas kepercayaan

Klik untuk melihat apa yang dipercaya dan apa yang tidak.

Klik setiap node untuk melihat fungsinya, keluarannya, dan pemeriksaan yang masih diperlukan.

BELUM DIPERCAYA

DIPERIKSA

Batas penting

NPA saat ini bukan pengganti praktis untuk Lean atau Rocq. Halaman ini menjelaskan desain riset yang berpusat pada sertifikat dan tidak menjamin sistem komersial bebas bug atau pembuktian teorema otomatis.

Pemeriksaan sertifikat / simulasi penjelasan

Ikuti alur pemeriksaan sertifikat.

Interaksi di peramban menjelaskan alur pemeriksaan. Ini tidak menjalankan NPA, Rust, WASM, atau sertifikat bukti sungguhan.

Contoh CLI

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

NPA / jejak audit SIAP

01 Baca sertifikatbyte kanonis / format TUNGGU
02 Periksa hash sertifikatcertificate_hash TUNGGU
03 Periksa dengan kernelpemeriksaan bukti dependen TUNGGU
04 Periksa ulang dengan pemeriksa acuanputusan tanpa sumber TUNGGU
05 Bandingkan laporan aksiomahash laporan aksioma TUNGGU

Putusan

Penjelasan belum dijalankan.

Jalankan penjelasan untuk memvisualkan langkah secara berurutan.

Ekosistem pembuktian

Perjelas peran, bukan memberi peringkat alat.

Lean dan Rocq adalah ekosistem asisten pembuktian yang matang. NPA ditampilkan di sini sebagai proyek riset dan implementasi yang berpusat pada sertifikat, bukan sebagai peringkat pengganti.

Item	Lean	Rocq	NPA
Posisi	Bahasa pemrograman dan asisten pembuktian sumber terbuka.	Pembukti teorema interaktif dengan sejarah riset yang panjang.	Repositori riset dan implementasi untuk pemeriksaan yang mengutamakan sertifikat.
Penggunaan umum	Matematika, verifikasi perangkat lunak, dan pemrograman.	Matematika, spesifikasi, verifikasi program, dan ekstraksi.	Riset tentang sertifikat bukti dan pemeriksaan independen.
Penekanan	Ekstensibilitas, pustaka, dan pembuktian interaktif.	Daya ungkap, metode matang, dan pustaka.	Basis tepercaya kecil dan sertifikat kanonis.
Cara halaman ini memperlakukannya	Acuan untuk pembelajaran, perbandingan, dan interoperabilitas.	Acuan untuk pembelajaran, perbandingan, dan metode formalisasi.	Proyek riset Finite Field.
Batas	Pengetahuan spesialis tetap diperlukan.	Pengetahuan spesialis tetap diperlukan.	Saat ini tidak dimaksudkan sebagai pengganti praktis untuk Lean atau Rocq.

Situs resmi Lean Situs resmi Rocq Prover GitHub NPA

Metode riset

Ubah “berhasil” menjadi prosedur pemeriksaan yang dapat diulang.

Hasil menjadi lebih kuat ketika orang lain dapat menjalankan ulang, memeriksa, dan menolaknya dalam kondisi yang sama.

Pertanyaan

Definisikan apa yang harus diperiksa: kinerja, kebenaran, kompatibilitas, atau cakupan.

Asumsi

Tulis asumsi, pengecualian, aksioma, celah data, dan bias sebelum evaluasi.

Artefak

Simpan sumber, sertifikat, masukan, log eksekusi, dan hash.

Pemeriksaan independen

Periksa hasil melalui jalur yang berbeda dari sisi pembuatan.

Tolok ukur

Tetapkan perangkat keras, versi, batas waktu, kumpulan instans, dan benih acak.

Batas

Publikasikan kegagalan, kasus yang tidak didukung, batas kinerja, dan validasi berikutnya.

Pembuat reproduksibilitas

Periksa apa yang masih kurang dari publikasi riset.

Daftar periksa diproses hanya di peramban. Ini bukan skor sertifikasi.

Kesiapan

Pertanyaan riset dan kondisi keberhasilanApa yang dihitung sebagai berhasil atau gagal. Alat dan dependensi yang ditetapkanVersi, berkas kunci, perangkat keras, dan lingkungan. Data masukan atau proses pembuatanAnonimisasi, lisensi, sumber, dan hash. Urutan perintah untuk menjalankan ulangDari inisialisasi sampai pembuatan hasil. Artefak yang dapat diperiksa dan log mentahSertifikat, laporan, log, dan hash. Batas, kegagalan, dan pertanyaan terbukaKasus yang tidak didukung dan masalah yang belum selesai.

Tindakan berikutnya

Definisikan pertanyaan riset dan kondisi keberhasilan lebih dulu.

Sebelum memutuskan format artefak, tetapkan apa yang akan dibandingkan atau diperiksa.

Artefak publik

Lacak artefak publik dari satu pintu masuk.

Halaman ini menghindari panggilan API GitHub saat eksekusi. Status repositori adalah cuplikan yang sudah ditinjau dan harus diperiksa sebelum publikasi.

4 artefak

finitefield-org

npa

rangkaian alat pembuktian yang mengutamakan sertifikat

Rust / OCamlApache-2.0Eksperimental

VERIFIKASI package verify-certs

finitefield-org

npa-std

paket teorema standar

BuktiPaketEksperimental

PERAN Std.Logic / Nat / List

finitefield-org

npa-mathlib

pustaka matematika formal

MatematikaBuktiRiset

PERAN paket teorema formal

GitHub

finitefield-org

indeks repositori publik

OrganisasiSumber terbuka

INDEKS semua repositori publik

Tidak ada artefak publik yang cocok dengan pencarian.

Kebijakan publikasi

Repositori publik, catatan riset, dan tolok ukur harus memuat tanggal pemeriksaan, kematangan, langkah reproduksi, dan batasan yang diketahui. Jumlah bintang dan komit tidak ditampilkan sebagai sinyal kualitas riset.

Dari Lab ke operasi

Bawa disiplin riset ke desain sistem bisnis.

Tidak semua sistem klien membutuhkan pembuktian teorema. Yang berguna untuk dibawa ke operasi adalah keputusan tentang apa yang harus dipercaya, dibandingkan, diperiksa, dikoreksi, dan disetujui manusia.

Praktik lab

Batas kepercayaan

Pisahkan pembuatan, perhitungan, dan pemeriksaan akhir, jangan mempercayai semua lapisan dengan bobot yang sama.

Bukti

Simpan masukan, keluaran, sertifikat, hash, dan log sebagai artefak yang dapat ditinjau.

Reproduksibilitas

Tetapkan data, versi, perintah, dan kriteria evaluasi sebelum membandingkan hasil.

Batas

Publikasikan kendala, kasus gagal, dan poin yang belum terselesaikan dengan bobot yang sama seperti hasil.

Sistem klien

Wewenang dan tanggung jawab

Definisikan siapa yang memasukkan data, siapa yang meninjau, siapa yang mengubah manual, dan siapa yang mengonfirmasi hasil.

Alasan keputusan

Tampilkan kendala, skor evaluasi, kandidat yang ditolak, dan poin yang belum selesai.

Keterlacakkan audit

Simpan perubahan kondisi, proses perhitungan, dan riwayat persetujuan akhir.

Penilaian manusia

Buat keluaran otomatis dapat dikoreksi, ditolak, dan dijelaskan kepada operator.

01 Shift dan penempatan staf

Tampilkan pelanggaran aturan dan pemenuhan preferensi secara terpisah.

02 Rute kendaraan

Jaga alasan rute, kapasitas, jendela waktu, dan pengecualian tetap terlihat.

03 Penjadwalan produksi

Jelaskan pekerjaan yang tidak terjadwal, hambatan, dan trade-off penyetelan.

04 Pencocokan penugasan

Tampilkan alasan kandidat dan alternatif sebelum persetujuan.

Catatan riset

Jaga riwayat pembaruan dan bukti tetap mudah dibaca.

Tidak semua kartu adalah artikel yang sudah diterbitkan. Catatan persiapan tetap tidak diberi label sebagai karya terbit sampai memiliki tanggal, sumber, dan langkah reproduksi.

NPA / Saat ini2026.06.21

Mengapa sertifikat ditempatkan di pusat

Mengapa bukti akhir sebaiknya berupa sertifikat standar yang diperiksa melalui jalur independen kecil.

Lihat repositori publik

Catatan desain / direncanakanSedang disiapkan

Membuat hasil optimasi dapat dijelaskan

Catatan desain tentang menampilkan tujuan, kendala keras, preferensi lunak, dan penugasan yang belum terselesaikan di antarmuka.

Lihat demo terkait

Tolok ukur / direncanakanSedang disiapkan

Kondisi untuk perbandingan pemecah yang adil

Catatan yang direncanakan tentang kumpulan instans, batas waktu, celah optimalitas, benih acak, dan perangkat keras.

Lihat kriteria publikasi

Item “Sedang disiapkan” bukan artikel terbit. Setelah publikasi, setiap catatan menerima tanggal, sumber, penulis, jalur reproduksi, dan batasan yang diketahui.

FAQ

Riset, alat pembuktian, dan batas penggunaan bisnis.

Poin-poin ini dibuat eksplisit agar halaman riset tidak disalahartikan sebagai jaminan produksi.

Baca tentang perusahaan

01 Apakah Math Lab adalah layanan pengembangan kontrak?

Tidak. Ini adalah tempat untuk menerbitkan sikap riset dan artefak. Dalam diskusi klien, kami memisahkan metode yang bisa diterapkan, metode yang masih perlu divalidasi, dan topik tahap riset.

02 Bisakah NPA menggantikan Lean atau Rocq?

Tidak. NPA saat ini bukan pengganti praktis untuk Lean atau Rocq. NPA adalah proyek riset dan implementasi tentang sertifikat, pemeriksaan independen, dan basis tepercaya yang kecil.

03 Apakah Anda mempercayai bukti yang dibuat AI begitu saja?

Tidak. AI, pencarian, dan taktik membantu membuat kandidat. Fokus kami adalah apakah sertifikat akhir diterima oleh pemeriksa yang independen dari jalur pembuatan tersebut.

04 Apakah verifikasi formal menghapus semua bug?

Tidak. Metode formal memeriksa sifat tertentu terhadap spesifikasi eksplisit. Spesifikasi yang salah, kode di luar cakupan, operasi, dan layanan eksternal tetap memerlukan tinjauan terpisah.

05 Apakah ini terkait dengan pekerjaan sistem bisnis?

Ya. Biasanya kami menerapkan disiplin ini bertahap: kendala, alasan hasil, riwayat perhitungan, batas izin, dan pemeriksaan untuk logika bisnis penting.

Diskusikan masalah

Anda dapat mendiskusikan pekerjaan yang ingin diselesaikan, bukan hanya topik riset.

Mulailah dari lembar kerja saat ini, aturan, dan titik keputusan yang dikoreksi manusia. Kami dapat menata apakah pemodelan matematis, otomasi aturan, atau prototipe harus didahulukan.

Periksa isu bisnis Lihat prototipe

Cuplikan sumber / 2026-06-21

Klaim NPA didasarkan pada cuplikan repositori finitefield-org/npa. Posisi Lean dan Rocq didasarkan pada situs resmi masing-masing. Status repositori, tag terbaru, dan kata-kata tinjauan metode diperiksa pada 2026-06-28.