Finite Field / Math Lab

Xây dựng bằng chứng về tính đúng đắn, không chỉ kết quả nhanh.

Math Lab là nơi chúng tôi trình bày cách xử lý mô hình toán học, chứng minh định lý, xác minh hình thức, khả năng tái lập và triển khai đáng tin cậy mà không phóng đại bằng chứng.

Xem lĩnh vực nghiên cứu Mở trang NPA

Dự án công khai: NPA / STD / MATHLIB
Ngôn ngữ lõi: Rust
Ảnh chụp NPA: v0.1.1

Kiểm toán chứng minh / góc nhìn khái niệm Chỉ đọc

01 byte chuẩn hóa / định dạng OK

02 certificate_hash OK

03 kiểm tra chứng minh phụ thuộc OK

04 kết luận không phụ thuộc mã nguồn OK

Ranh giới tin cậy được hiển thị

Trang này không tuyên bố NPA là phương án thay thế thực tế cho Lean hoặc Rocq, và mô phỏng trong trình duyệt không thực thi NPA.

Nguyên tắc Lab

Công bố không chỉ kết quả mà cả ranh giới kiểm tra.

Một kết luận như “đã chạy được”, “rất nhanh” hoặc “đã được chứng minh” là chưa đủ. Chúng tôi tách riêng đầu vào, giả định, phần được tin cậy, hiện vật có thể kiểm tra độc lập và vấn đề chưa giải quyết.

01 / Ranh giới

Giữ nền tin cậy nhỏ

Không đặt bộ tạo phức tạp hoặc AI vào trung tâm của niềm tin. Hãy làm rõ phía kiểm tra nhỏ.

02 / Bằng chứng

Biến bằng chứng thành hiện vật

Để chứng chỉ, hàm băm, danh sách giả định, điều kiện đánh giá chuẩn và nhật ký ở dạng người khác có thể kiểm tra.

03 / Tái lập

Thiết kế để có thể tái lập

Cố định chuỗi công cụ, dữ liệu đầu vào, lệnh thực thi và tiêu chí để kết quả có thể được kiểm tra lại.

04 / Trung thực

Không phóng đại trạng thái nghiên cứu

Hiển thị riêng phương pháp thực tế, thử nghiệm và nghiên cứu. Đặt giới hạn cạnh kết quả.

RÀ SOÁT PHƯƠNG PHÁP

Nhóm phương pháp dịch vụ vẫn cần phạm vi, trách nhiệm, bằng chứng từ khách hàng và phê duyệt trước khi được mô tả là sẵn sàng cho dự án.

THỬ NGHIỆM

Đã có triển khai hoạt động, nhưng quy mô, khả năng tương thích, hiệu năng hoặc thay đổi đặc tả vẫn có thể xảy ra. Cần phiên bản và bước tái lập.

NGHIÊN CỨU

Thiết kế, đánh giá, chứng minh hoặc triển khai vẫn đang tiếp diễn. Điều này không hàm ý đã sẵn sàng thương mại hoặc đã hoàn tất.

Danh mục nghiên cứu

Xem nghiên cứu theo mức trưởng thành và hiện vật.

Mỗi thẻ hiển thị mức trưởng thành, hiện vật, trạng thái hiện tại và bước xác minh tiếp theo. Tìm kiếm và bộ lọc chỉ dùng trạng thái phía trình duyệt.

8 mục hiển thị

THỬ NGHIỆM MÃ NGUỒN MỞ

Nano Proof Auditor

Chuỗi công cụ chứng minh ưu tiên chứng chỉ

Chuỗi công cụ nghiên cứu đặt chứng chỉ chứng minh chuẩn hóa và nền kiểm tra nhỏ ở trung tâm của việc rà soát chứng minh phụ thuộc.

Hiện vật: mã nguồn / đặc tả / mẫu CI
Hiện tại: ảnh chụp công khai v0.1.1
Xác minh tiếp theo: gói định lý bên ngoài và kiểm tra độc lập

Mở chi tiết NPA

THỬ NGHIỆM MÃ NGUỒN MỞ

Thư viện chuẩn NPA

Logic / Nat / List / Algebra

Kho gói định lý chuẩn cho các nền tảng NPA có thể tái sử dụng.

Hiện vật: mã nguồn / gói chứng minh
Hiện tại: kho công khai đã tách
Xác minh tiếp theo: phạm vi gói và khả năng tương thích

GitHub

NGHIÊN CỨU MÃ NGUỒN MỞ

Thư viện toán học NPA

Thư viện toán học hình thức

Hướng thư viện để lưu định lý toán học dưới dạng gói chứng minh có thể kiểm tra độc lập.

Hiện vật: mã nguồn / gói chứng minh
Hiện tại: kho công khai đang phát triển
Xác minh tiếp theo: cấu trúc thư viện và kiểm toán phụ thuộc

GitHub

RÀ SOÁT PHƯƠNG PHÁP PHƯƠNG PHÁP

Mô hình lập kế hoạch có ràng buộc

Lập lịch / Định tuyến / Phân công

Phương pháp tách ràng buộc cứng và chỉ số đánh giá trong công việc ca làm, thăm hiện trường, định tuyến, sản xuất và phân công.

Hiện vật: mô hình / nguyên mẫu / báo cáo giải thích
Hiện tại: phương pháp dịch vụ; tuyên bố công khai giới hạn ở rà soát phương pháp
Xác minh tiếp theo: bằng chứng từ khách hàng và phê duyệt phạm vi

Xem nguyên mẫu

NGHIÊN CỨU ĐO LƯỜNG

Đánh giá bộ giải có thể tái lập

Đánh giá chuẩn và bằng chứng

Chương trình cố định bộ trường hợp, phần cứng, giới hạn thời gian, hạt ngẫu nhiên và nhật ký thô trước khi đưa ra tuyên bố hiệu năng.

Hiện vật: sổ đăng ký đánh giá chuẩn / nhật ký thô / báo cáo
Hiện tại: thiết kế chương trình nghiên cứu
Xác minh tiếp theo: bộ dữ liệu đánh giá chuẩn công khai đầu tiên

Xem phương pháp

NGHIÊN CỨU PHƯƠNG PHÁP HÌNH THỨC

Xác minh logic nghiệp vụ trọng yếu

Bất biến cho hệ thống nghiệp vụ

Nghiên cứu về cách tách phí, quyền hạn, tồn kho và chuyển trạng thái thành đặc tả và bất biến.

Hiện vật: đặc tả / bất biến / báo cáo kiểm thử hoặc chứng minh
Hiện tại: nghiên cứu phạm vi
Xác minh tiếp theo: chọn một trường hợp gần sản xuất có phạm vi giới hạn

Xem thiết kế bảo mật

THỬ NGHIỆM KỸ THUẬT

Thành phần tin cậy nhỏ trong Rust

Thành phần tin cậy nhỏ

Công việc triển khai giữ các phần trọng yếu về tin cậy như bộ kiểm tra và hàm băm đủ nhỏ để kiểm tra.

Hiện vật: lõi NPA / gói chứng chỉ / bộ kiểm tra tham chiếu
Hiện tại: triển khai công khai trong NPA
Xác minh tiếp theo: khả năng tương thích với bộ kiểm tra độc lập

Xem mã nguồn

NGHIÊN CỨU AI × CHỨNG MINH

Hỗ trợ bằng AI và kiểm tra độc lập

Tạo tự do, kiểm tra nghiêm ngặt

Hướng nghiên cứu đặt AI ở bước tạo ứng viên, còn bằng chứng cuối cùng được kiểm tra độc lập.

Hiện vật: bộ tạo ứng viên / chứng chỉ / báo cáo kiểm tra
Hiện tại: hướng nghiên cứu phù hợp với mô hình tin cậy của NPA
Xác minh tiếp theo: quy trình soạn thảo được đo lường

Xem ranh giới tin cậy

Không tìm thấy lĩnh vực nghiên cứu phù hợp.

Thử từ khóa khác hoặc đưa bộ lọc mức trưởng thành về tất cả.

Nano Proof Auditor

Tách việc tạo chứng minh khỏi phần được tin cậy.

NPA là chuỗi công cụ chứng minh ưu tiên chứng chỉ cho chứng minh phụ thuộc. Giao diện nhập liệu, chiến thuật, tìm kiếm định lý, phần bổ trợ, AI, tệp nguồn và trạng thái CI có thể giúp tạo ứng viên, nhưng không phải bằng chứng chứng minh đáng tin cậy.

THỬ NGHIỆMMÃ NGUỒN MỞAPACHE-2.0

Ảnh chụp hiện tại

v0.1.1

Thông tin công khai đã được kiểm tra ngày 2026-06-21.

Lõi chính

Rust

Bộ xác minh Rust và lõi kiểm tra thuộc phía kiểm tra.

Hiện vật kiểm toán

.npcert

Các byte chứng chỉ chuẩn hóa là đối tượng cần kiểm tra.

Điểm kiểm tra lại

manual review

Trạng thái kho và khả năng hiển thị gói phải được rà soát trước khi công bố.

Trình khám phá ranh giới tin cậy

Bấm qua để xem điều gì được tin cậy và điều gì không.

Bấm từng nút để xem nó làm gì, tạo ra gì và vẫn cần kiểm tra nào.

UNTRUSTED

CHECKED

Ranh giới quan trọng

NPA hiện chưa phải phương án thay thế thực tế cho Lean hoặc Rocq. Trang này giải thích thiết kế nghiên cứu lấy chứng chỉ làm trung tâm và không bảo đảm hệ thống thương mại không lỗi hay tự động giải định lý.

Kiểm tra chứng chỉ / mô phỏng giải thích

Xem luồng kiểm tra chứng chỉ.

Tương tác trong trình duyệt giải thích luồng kiểm tra. Nó không chạy NPA, Rust, WASM hay chứng chỉ chứng minh thật.

Ví dụ CLI

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

NPA / dấu vết kiểm toán SẴN SÀNG

01 Đọc chứng chỉbyte chuẩn hóa / định dạng CHỜ
02 Kiểm tra hàm băm chứng chỉcertificate_hash CHỜ
03 Kiểm tra bằng lõi kiểm trakiểm tra chứng minh phụ thuộc CHỜ
04 Kiểm tra lại bằng bộ kiểm tra tham chiếukết luận không phụ thuộc mã nguồn CHỜ
05 So sánh báo cáo tiên đềhàm băm báo cáo tiên đề CHỜ

Kết luận

Phần giải thích chưa chạy.

Chạy phần giải thích để xem các bước theo thứ tự.

Hệ sinh thái chứng minh

Làm rõ vai trò thay vì xếp hạng công cụ.

Lean và Rocq là các hệ sinh thái trợ lý chứng minh đã trưởng thành. NPA được trình bày ở đây như một dự án nghiên cứu và triển khai xoay quanh chứng chỉ, không phải bảng xếp hạng thay thế.

Mục	Lean	Rocq	NPA
Vị trí	Ngôn ngữ lập trình mã nguồn mở và trợ lý chứng minh.	Bộ chứng minh định lý tương tác có lịch sử nghiên cứu lâu dài.	Kho nghiên cứu và triển khai cho kiểm tra lấy chứng chỉ làm trung tâm.
Cách dùng điển hình	Toán học, xác minh phần mềm và lập trình.	Toán học, đặc tả, xác minh chương trình và trích xuất.	Nghiên cứu về chứng chỉ chứng minh và kiểm tra độc lập.
Trọng tâm	Khả năng mở rộng, thư viện và chứng minh tương tác.	Khả năng biểu đạt, phương pháp trưởng thành và thư viện.	Nền tin cậy nhỏ và chứng chỉ chuẩn hóa.
Cách trang này nhìn nhận	Tham chiếu để học hỏi, so sánh và tương tác.	Tham chiếu để học hỏi, so sánh và phương pháp hình thức hóa.	Dự án nghiên cứu của Finite Field.
Ranh giới	Vẫn cần kiến thức chuyên môn.	Vẫn cần kiến thức chuyên môn.	Hiện tại không nhằm thay thế Lean hoặc Rocq trong thực tế.

Trang chính thức của Lean Trang chính thức của Rocq Prover NPA trên GitHub

Phương pháp nghiên cứu

Biến “đã chạy được” thành quy trình kiểm tra có thể lặp lại.

Một kết quả đáng tin hơn khi người khác có thể chạy lại, kiểm tra và bác bỏ nó trong cùng điều kiện.

Câu hỏi

Xác định điều cần kiểm tra: hiệu năng, tính đúng đắn, khả năng tương thích hoặc phạm vi.

Giả định

Viết rõ giả định, loại trừ, tiên đề, thiếu hụt dữ liệu và thiên lệch trước khi đánh giá.

Hiện vật

Giữ mã nguồn, chứng chỉ, đầu vào, nhật ký thực thi và hàm băm.

Kiểm tra độc lập

Kiểm tra kết quả qua một đường khác với phía tạo sinh.

Đánh giá chuẩn

Cố định phần cứng, phiên bản, giới hạn thời gian, bộ trường hợp và hạt ngẫu nhiên.

Giới hạn

Công bố thất bại, trường hợp chưa hỗ trợ, giới hạn hiệu năng và bước xác minh tiếp theo.

Bộ dựng khả năng tái lập

Kiểm tra công bố nghiên cứu còn thiếu gì.

Danh sách kiểm tra chỉ được xử lý trong trình duyệt. Đây không phải điểm chứng nhận.

Mức sẵn sàng

Câu hỏi nghiên cứu và điều kiện thành côngĐiều gì được tính là thành công hoặc thất bại. Công cụ và phụ thuộc đã cố địnhPhiên bản, tệp khóa, phần cứng và môi trường. Dữ liệu đầu vào hoặc quy trình tạo dữ liệuẨn danh hóa, giấy phép, nguồn và hàm băm. Chuỗi lệnh chạy lạiTừ khởi tạo đến tạo kết quả. Hiện vật có thể kiểm tra và nhật ký thôChứng chỉ, báo cáo, nhật ký và hàm băm. Giới hạn, thất bại và câu hỏi còn mởTrường hợp chưa hỗ trợ và vấn đề chưa giải quyết.

Hành động tiếp theo

Trước hết hãy xác định câu hỏi nghiên cứu và điều kiện thành công.

Trước khi quyết định định dạng hiện vật, hãy cố định điều sẽ được so sánh hoặc kiểm tra.

Hiện vật công khai

Theo dõi hiện vật công khai từ một lối vào.

Trang này tránh gọi GitHub API khi chạy. Trạng thái kho là ảnh chụp đã rà soát và phải được kiểm tra trước khi công bố.

4 hiện vật

finitefield-org

npa

chuỗi công cụ chứng minh ưu tiên chứng chỉ

Rust / OCamlApache-2.0Thử nghiệm

XÁC MINH package verify-certs

finitefield-org

npa-std

gói định lý chuẩn

Chứng minhGóiThử nghiệm

VAI TRÒ Std.Logic / Nat / List

finitefield-org

npa-mathlib

thư viện toán học hình thức

Toán họcChứng minhNghiên cứu

VAI TRÒ gói định lý hình thức

GitHub

finitefield-org

chỉ mục kho công khai

Tổ chứcMã nguồn mở

CHỈ MỤC tất cả kho công khai

Không có hiện vật công khai nào khớp với tìm kiếm.

Chính sách công bố

Kho công khai, ghi chú nghiên cứu và đánh giá chuẩn nên có ngày kiểm tra, mức trưởng thành, bước tái lập và giới hạn đã biết. Số sao và số commit không được hiển thị như tín hiệu chất lượng nghiên cứu.

Từ phòng thí nghiệm đến vận hành

Đưa kỷ luật nghiên cứu vào thiết kế hệ thống nghiệp vụ.

Không phải hệ thống khách hàng nào cũng cần chứng minh định lý. Giá trị thực tế là xác định điều gì cần được tin cậy, so sánh, kiểm tra, chỉnh sửa và được con người phê duyệt.

Thực hành trong phòng thí nghiệm

Ranh giới tin cậy

Tách bước tạo sinh, tính toán và kiểm tra cuối cùng, thay vì tin mọi lớp như nhau.

Bằng chứng

Giữ đầu vào, đầu ra, chứng chỉ, hàm băm và nhật ký như các hiện vật có thể rà soát.

Khả năng tái lập

Cố định dữ liệu, phiên bản, lệnh và tiêu chí đánh giá trước khi so sánh kết quả.

Giới hạn

Công bố ràng buộc, trường hợp thất bại và điểm chưa giải quyết với cùng mức trọng tâm như kết quả.

Hệ thống khách hàng

Thẩm quyền và trách nhiệm

Xác định ai nhập dữ liệu, ai rà soát, ai ghi đè và ai xác nhận kết quả.

Lý do quyết định

Hiển thị ràng buộc, điểm đánh giá, phương án bị loại và điểm chưa giải quyết.

Khả năng kiểm toán

Lưu lại thay đổi điều kiện, lần chạy tính toán và lịch sử phê duyệt cuối cùng.

Phán đoán của con người

Làm cho kết quả tự động có thể được chỉnh sửa, từ chối và giải thích cho người vận hành.

01 Ca làm và bố trí nhân sự

Hiển thị riêng phần vi phạm quy tắc và phần đáp ứng ưu tiên.

02 Định tuyến xe

Giữ lý do tuyến đường, năng lực, khung thời gian và ngoại lệ ở trạng thái nhìn thấy được.

03 Lập lịch sản xuất

Giải thích công việc chưa lập lịch, điểm nghẽn và đánh đổi khi thiết lập.

04 Ghép phân công

Hiển thị lý do của phương án đề xuất và các phương án thay thế trước khi phê duyệt.

Ghi chú nghiên cứu

Giữ lịch sử cập nhật và bằng chứng ở dạng dễ đọc.

Không phải thẻ nào cũng là bài viết đã xuất bản. Các ghi chú đang chuẩn bị chưa được gắn là nội dung đã công bố cho đến khi có ngày, nguồn và bước tái lập.

NPA / Hiện tại2026.06.21

Vì sao đặt chứng chỉ ở trung tâm

Vì sao bằng chứng cuối cùng nên là chứng chỉ chuẩn hóa được kiểm tra bằng một đường nhỏ độc lập.

Xem kho công khai

Ghi chú thiết kế / dự kiếnĐang chuẩn bị

Làm cho kết quả tối ưu hóa có thể giải thích được

Ghi chú thiết kế về cách hiển thị mục tiêu, ràng buộc cứng, ưu tiên mềm và phân công chưa giải quyết trong giao diện.

Xem bản demo liên quan

Đánh giá chuẩn / dự kiếnĐang chuẩn bị

Điều kiện để so sánh bộ giải công bằng

Ghi chú dự kiến về bộ trường hợp, giới hạn thời gian, khoảng cách tối ưu, hạt ngẫu nhiên và phần cứng.

Xem tiêu chí công bố

Các mục “Đang chuẩn bị” không phải bài viết đã xuất bản. Sau khi công bố, mỗi ghi chú sẽ có ngày, nguồn, tác giả, đường tái lập và giới hạn đã biết.

Câu hỏi thường gặp

Ranh giới giữa nghiên cứu, công cụ chứng minh và sử dụng trong nghiệp vụ.

Các điểm này được làm rõ để trang nghiên cứu không bị hiểu nhầm là cam kết sản xuất.

Đọc về công ty

01 Math Lab có phải dịch vụ phát triển theo hợp đồng không?

Không. Đây là nơi công bố lập trường nghiên cứu và hiện vật. Trong trao đổi với khách hàng, chúng tôi tách phương pháp có thể áp dụng, phương pháp cần xác minh thêm và chủ đề còn ở giai đoạn nghiên cứu.

02 NPA có thể thay thế Lean hoặc Rocq không?

Không. NPA hiện tại không phải phương án thay thế thực tế cho Lean hoặc Rocq. Đây là dự án nghiên cứu và triển khai về chứng chỉ, kiểm tra độc lập và nền tin cậy nhỏ.

03 Bạn có tin nguyên trạng các chứng minh do AI tạo ra không?

Không. AI, tìm kiếm và chiến thuật giúp tạo phương án ứng viên. Chúng tôi tập trung vào việc chứng chỉ cuối cùng có được bộ kiểm tra độc lập với các đường tạo sinh đó chấp nhận hay không.

04 Xác minh hình thức có loại bỏ mọi lỗi không?

Không. Phương pháp hình thức kiểm tra các thuộc tính cụ thể theo đặc tả rõ ràng. Đặc tả sai, mã ngoài phạm vi, vận hành và dịch vụ bên ngoài vẫn cần rà soát riêng.

05 Điều này có liên quan đến công việc hệ thống nghiệp vụ không?

Có. Chúng tôi thường áp dụng kỷ luật này từng bước: ràng buộc, lý do kết quả, lịch sử tính toán, ranh giới quyền hạn và kiểm tra logic nghiệp vụ quan trọng.

Trao đổi về vấn đề

Bạn có thể trao đổi về công việc cần giải quyết, không chỉ về chủ đề nghiên cứu.

Hãy bắt đầu từ bảng tính hiện tại, quy tắc và những điểm quyết định còn được con người chỉnh sửa. Chúng tôi có thể cùng xác định nên bắt đầu bằng mô hình toán học, tự động hóa quy tắc hay nguyên mẫu.

Kiểm tra vấn đề nghiệp vụ Xem nguyên mẫu

Ảnh chụp nguồn / 2026-06-21

Các tuyên bố về NPA dựa trên ảnh chụp kho finitefield-org/npa. Vị trí của Lean và Rocq dựa trên trang chính thức của chúng. Trạng thái kho, thẻ phát hành mới nhất và cách diễn đạt về rà soát phương pháp đã được kiểm tra ngày 2026-06-28.