สถานะสาธารณะ
รีโพซิทอรีวิจัยและการพัฒนา
รีโพซิทอรี GitHub เป็นสาธารณะ แต่หน้านี้อธิบายรีโพซิทอรีวิจัยและพัฒนา ไม่ใช่บริการที่เปิดใช้งานแล้ว
กลับไปที่ Math Lab
NPA / การตรวจ proof ที่ให้ใบรับรองมาก่อน
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 ค่า pin ใน 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 จาก metadata LICENSE สาธารณะเมื่อ 2026-07-02
ขอบเขต
NPA ไม่ใช่สิ่งทดแทน Lean หรือ Rocq ในทางปฏิบัติ การจำลองตรวจในเบราว์เซอร์ที่เผยแพร่ไม่ได้รัน NPA จริง แท็กสาธารณะ ใบอนุญาต และการมองเห็นรีโพซิทอรีตรวจเมื่อ 2026-07-02 สำหรับการอ่านทวนก่อนเผยแพร่ขั้นสุดท้าย
ขอบเขตความเชื่อถือ
ย้ายเฉพาะใบรับรองมาตรฐานข้ามขอบเขตหลักฐาน
ขอบเขตนี้ไม่ได้เกี่ยวกับเครื่องมือใดดูซับซ้อนกว่า แต่เกี่ยวกับหลักฐานใดได้รับอนุญาตให้กลายเป็นหลักฐานหลังการตรวจอิสระ
Parser, elaborator, tactics, automation, การค้นหาทฤษฎีบท, ปลั๊กอิน, ระบบ AI, ไฟล์ซอร์ส, ไฟล์ replay, ดัชนีทฤษฎีบท, แผนเผยแพร่, สถานะ CI, หน้ารุ่นเผยแพร่ และ metadata registry อยู่ฝั่งตัวเลือกที่ยังไม่เชื่อถือ
ลำดับการพิสูจน์ / การจำลองเพื่ออธิบาย
แสดงลำดับที่แน่ชัดจากไบต์ใบรับรองถึงหลักฐานการตรวจ
การจำลองในเบราว์เซอร์ไม่ได้รัน NPA, Rust, WASM หรือใบรับรองการพิสูจน์จริง แต่แสดงลำดับการตรวจที่ไม่พึ่งซอร์สซึ่งหลักฐานจริงต้องผ่าน
เส้นทางหลักฐาน CLI
npa package verify-certs --root . --checker reference --json
NPA / ร่องรอยการตรวจย้อนหลัง
พร้อม
- 01 รูปแบบใบรับรองไบต์ .npcert แบบมาตรฐาน / ใบรับรองที่อ่านโครงสร้างได้ / ตรวจรูปแบบ รอ
- 02 แฮชใบรับรองไบต์ใบรับรอง / certificate_hash / ผลย่อยืนยันแบบกำหนดผลได้ รอ
- 03 ผลตัดสินของแกนตรวจใบรับรอง / ยอมรับหรือปฏิเสธ / รายงานตัวตรวจสอบ Rust รอ
- 04 ตัวตรวจอ้างอิงใบรับรองที่ตรึงด้วยแฮช / ผลยอมรับหรือปฏิเสธอิสระ / รายงานตัวตรวจที่ไม่พึ่งซอร์ส รอ
- 05 รายงานสัจพจน์แพ็กเกจที่ตรวจแล้ว / axiom_report_hash / บัญชีสมมติฐาน รอ
ผลตัดสิน
ยังไม่ได้รันลำดับคำอธิบายรันคำอธิบายเพื่อทำเครื่องหมายเส้นทางตรวจที่ไม่พึ่งซอร์สตามลำดับ
ทะเบียนคำกล่าว
แยกหลักฐาน ข้อเท็จจริงที่ไวต่อเวลา และคำกล่าวเรื่องขอบเขต
หน้านี้ไม่พึ่งถ้อยคำวิจัยหลวมๆ คำกล่าวสาธารณะแต่ละรายการผูกกับภาพรวมข้อเท็จจริงภายใน แหล่งข้อมูล และการดำเนินการเผยแพร่
| คำกล่าว | ถ้อยคำสาธารณะ | สถานะ | แหล่งที่มา | การดำเนินการเผยแพร่ |
|---|---|---|---|---|
| CL-001 | NPA ให้ใบรับรองมาก่อน: ขอบเขตที่ audit ได้คือหลักฐาน .npcert แบบมาตรฐานและเส้นทางตรวจรอบหลักฐานนั้น | ตรวจคำกล่าวสาธารณะแล้ว | S01 / 2026-07-02 | ทบทวนเมื่อ README เปลี่ยน |
| CL-002 | การตรวจสาธารณะซ้ำเมื่อ 2026-07-02 พบว่าแท็ก git ล่าสุดของรีโพซิทอรี NPA คือ v0.2.0 README ของแพ็กเกจที่เกี่ยวข้องยังแสดง pin เฉพาะรีโพซิทอรี จึงจำกัดถ้อยคำเวอร์ชันตามรีโพซิทอรี | ตรวจสาธารณะซ้ำแล้ว | S01 / S02 / 2026-07-02 | จำกัดถ้อยคำแท็กตามรีโพซิทอรี |
| CL-003 | ภาพรวมข้อเท็จจริงภายในบันทึกการตรึง toolchain Rust 1.95.0 และไม่ได้ใช้เป็นคำกล่าวทางการตลาด | ตรวจแล้วและไวต่อเวลา | S01 / 2026-07-02 | ตรวจซ้ำหากแสดงเวอร์ชัน toolchain |
| 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 ผ่าน metadata LICENSE สาธารณะ | ตรวจคำกล่าวสาธารณะแล้ว | S01 / S02 / 2026-07-02 | ตรวจ LICENSE ซ้ำเมื่อมีรุ่นใหญ่ |
รีโพซิทอรีและใบอนุญาต
ทำให้โค้ด รีโพซิทอรีแพ็กเกจ และการมองเห็นองค์กรชัดเจน
ลิงก์รีโพซิทอรีเป็นจุดอ้างอิงแหล่งโค้ดสาธารณะ ไม่ใช่การรับประกันว่าหน้านี้ซิงก์กับสถานะ GitHub ล่าสุดตลอดเวลา
4 รีโพซิทอรี
finitefield-org
npa
ชุดเครื่องมือช่วยพิสูจน์และตรวจสอบที่ให้ใบรับรองมาก่อน
- ใบอนุญาต
- ตรวจ Apache-2.0 จาก LICENSE เมื่อ 2026-07-02
- การตรวจยืนยัน
- แท็ก git ล่าสุด: v0.2.0 ยังไม่มี GitHub release ล่าสุดที่เผยแพร่ ค่า toolchain ใน README ปัจจุบัน: NPA_GIT_TAG=v0.2.0
ทดลองRust / OCamlให้ใบรับรองมาก่อน
เปิดรีโพซิทอรี
finitefield-org
npa-std
รีโพซิทอรีแพ็กเกจทฤษฎีบทมาตรฐานสำหรับซอร์ส proof ของ NPA
- ใบอนุญาต
- ตรวจ Apache-2.0 จาก LICENSE เมื่อ 2026-07-02
- การตรวจยืนยัน
- แท็ก git ล่าสุดและ GitHub release: v0.1.0 metadata เวอร์ชันแพ็กเกจใน README: 0.1.0; pin toolchain ของแพ็กเกจ: NPA_GIT_TAG=v0.1.1
ทดลองแพ็กเกจทฤษฎีบทซอร์ส proof
เปิดรีโพซิทอรี
finitefield-org
npa-mathlib
รีโพซิทอรีวิจัยคลังคณิตศาสตร์เชิงรูปแบบ
- ใบอนุญาต
- ตรวจ Apache-2.0 จาก LICENSE เมื่อ 2026-07-02
- การตรวจยืนยัน
- แท็ก git ล่าสุด: v0.1.30 GitHub release ล่าสุด: v0.1.9 metadata เวอร์ชันแพ็กเกจใน README: 0.2.1; pin toolchain ของแพ็กเกจ: NPA_GIT_TAG=v0.1.1
วิจัยคณิตศาสตร์เชิงรูปแบบคลัง
เปิดรีโพซิทอรี
finitefield-org
Finite Field GitHub organization
ภาพรวมองค์กรสาธารณะสำหรับตระกูลรีโพซิทอรีของแล็บ
- ใบอนุญาต
- ใช้ใบอนุญาตเฉพาะแต่ละรีโพซิทอรี
- การตรวจยืนยัน
- npa, npa-std และ npa-mathlib เป็นสาธารณะตามการอ่านผ่าน GitHub API เมื่อ 2026-07-02
ดัชนีสาธารณะภาพรวมการมองเห็นซอร์ส
เปิดองค์กร
ไม่มีรีโพซิทอรีที่ตรงกับการค้นหาปัจจุบัน
รีโพซิทอรี GitHub เป็นแหล่งข้อมูลสำหรับสถานะโค้ดสาธารณะ ใบอนุญาต แท็กปัจจุบัน การมองเห็นสาธารณะ และถ้อยคำรุ่นเผยแพร่ตรวจเมื่อ 2026-07-02 เป็นการอ่านทวนขั้นสุดท้ายของ M10-T14
กรอบป้องกันความเข้าใจผิดของระบบนิเวศ proof
ทำให้บทบาทชัดเจนก่อนเปรียบเทียบเครื่องมือพิสูจน์
ตารางนี้เป็นตารางบทบาท ไม่ใช่การจัดอันดับ Lean และ Rocq ยังคงเป็นระบบนิเวศผู้ช่วยพิสูจน์สำหรับอ้างอิง ส่วน NPA นำเสนอเป็นงานวิจัยและพัฒนาที่เน้นใบรับรอง
| รายการ | Lean | Rocq | NPA |
|---|---|---|---|
| ตำแหน่ง | ภาษาโปรแกรมและผู้ช่วยพิสูจน์แบบโอเพนซอร์ส | เครื่องพิสูจน์ทฤษฎีบทแบบโต้ตอบที่มีประวัติการวิจัยยาวนาน | รีโพซิทอรีวิจัยและพัฒนาสำหรับการตรวจที่ให้ใบรับรองมาก่อน |
| การใช้งานทั่วไป | คณิตศาสตร์ การตรวจสอบซอฟต์แวร์ และการเขียนโปรแกรม | คณิตศาสตร์ ข้อกำหนด การตรวจสอบโปรแกรม และการดึงโปรแกรมออกจาก proof | งานวิจัยเรื่องใบรับรองการพิสูจน์ การตรวจอิสระ และฐานที่ต้องเชื่อถือขนาดเล็ก |
| ขอบเขตหลักฐาน | แกนตรวจและระบบนิเวศที่เชื่อถือของตนกำหนดขอบเขตการตรวจ | แกนตรวจและงานพัฒนาที่ผ่านการตรวจของตนกำหนดขอบเขตการตรวจ | หลักฐาน .npcert แบบมาตรฐานข้ามจากการสร้างเข้าสู่การตรวจ |
| บทบาทในหน้านี้ | แหล่งอ้างอิงสำหรับการเรียนรู้ เปรียบเทียบ และทำงานร่วมกับระบบอื่น | แหล่งอ้างอิงสำหรับการเรียนรู้ เปรียบเทียบ และวิธีทำให้ข้อกำหนดเป็นรูปแบบทางการ | โครงการวิจัยของ Finite Field ไม่ใช่คำสัญญาของผลิตภัณฑ์ |
| ขอบเขต | ยังต้องใช้ความรู้เฉพาะทาง | ยังต้องใช้ความรู้เฉพาะทาง | ขณะนี้ NPA ไม่ใช่สิ่งทดแทน Lean หรือ Rocq ในทางปฏิบัติ |
แหล่งข้อมูล
เผยแพร่แผนที่แหล่งข้อมูลไว้ข้างการตีความ
แสดงแหล่งข้อมูลเพื่อให้ผู้อ่านเห็นว่าคำกล่าวใดมาจากรีโพซิทอรีสาธารณะ เว็บไซต์ทางการของเครื่องมือพิสูจน์ และบริบทธุรกิจของบริษัท
S01
finitefield-org/npa
แหล่งข้อมูลหลักสำหรับเป้าหมายของ NPA โมเดลความเชื่อถือ ถ้อยคำแท็กรีโพซิทอรีปัจจุบัน v0.2.0 คำสั่ง โครงสร้างรีโพซิทอรี และใบอนุญาต
เปิดแหล่งข้อมูล S02องค์กร GitHub ของ Finite Field
แหล่งข้อมูลหลักสำหรับการมองเห็นรีโพซิทอรีสาธารณะ แท็ก 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 ข้อเท็จจริงใดต้องตรวจซ้ำ
เวอร์ชันสาธารณะปัจจุบัน การมองเห็นรีโพซิทอรี ค่า pin ของ toolchain ข้อความใบอนุญาต และถ้อยคำในซอร์ส ตรวจซ้ำเมื่อ 2026-07-02
จากวินัยของการพิสูจน์สู่การปฏิบัติงาน
ใช้วินัยด้านหลักฐานแบบเดียวกันเมื่อการตัดสินใจทางธุรกิจต้องเชื่อถือได้
สำหรับระบบธุรกิจ บทเรียนที่มีประโยชน์ไม่ใช่การเพิ่มการพิสูจน์ทฤษฎีบททุกที่ แต่คือการตัดสินใจว่าอะไรต้องถูกสร้าง ตรวจ บันทึก แก้ไข และอนุมัติโดยคน