01 / 경계
신뢰 기반을 작게 유지
복잡한 생성기나 AI를 신뢰의 중심에 두지 않습니다. 작은 확인 쪽을 명확히 드러냅니다.
Finite Field / 수학 랩
빠른 결과뿐 아니라 정확성의 증거를구축합니다.
수학 랩은 수학적 모델링, 정리 증명, 형식 검증, 재현성, 신뢰할 수 있는 구현을 다루는 방식을 증거를 과장하지 않고 보여주는 공간입니다.
- 공개 프로젝트
- NPA / STD / MATHLIB
- 핵심 언어
- Rust
- NPA 스냅샷
- v0.1.1
증명 감사 / 개념도
읽기 전용
01 표준 바이트 / 형식 정상
02 인증서 해시 정상
03 종속 증명 확인 정상
04 원본 없는 판정 정상
신뢰 경계를 보이게 합니다
이 페이지는 NPA가 Lean이나 Rocq의 실무적 대체물이라고 주장하지 않으며, 브라우저 시뮬레이션은 NPA를 실행하지 않습니다.
랩 원칙
결과뿐 아니라 확인의 경계도 공개합니다.
“작동했다”, “빨랐다”, “증명됐다”라는 결론만으로는 충분하지 않습니다. 입력, 가정, 신뢰하는 부분, 독립적으로 확인 가능한 산출물, 미해결 문제를 따로 보여줍니다.
02 / 증거
증거를 산출물로 남기기
인증서, 해시, 가정 목록, 벤치마크 조건, 로그를 다른 사람이 검사할 수 있는 형태로 남깁니다.
03 / 재현
재현성을 염두에 두고 설계
결과를 다시 확인할 수 있도록 도구 체인, 입력 데이터, 실행 명령, 기준을 고정합니다.
04 / 정직성
연구 상태를 과장하지 않기
실무 방법, 실험, 연구를 구분해서 보여줍니다. 한계는 결과 옆에 둡니다.
방법 검토
프로젝트 준비 완료라고 설명하기 전에 범위, 책임, 고객 증거, 승인이 더 필요한 서비스 방법 범주입니다.
실험
작동하는 구현은 있지만 규모, 호환성, 성능 또는 명세 변경 가능성이 남아 있습니다. 버전과 재현 단계가 필요합니다.
연구
설계, 평가, 증명 또는 구현이 진행 중입니다. 상용 제공이나 완료를 의미하지 않습니다.
연구 포트폴리오
성숙도와 산출물 기준으로 연구를 봅니다.
각 카드는 성숙도, 산출물, 현재 상태, 다음 검증을 보여줍니다. 검색과 필터는 브라우저 안의 상태만 사용합니다.
8개 표시
실험
오픈소스
01
Nano Proof Auditor
인증서 우선 증명 도구 체인
표준 증명 인증서와 작은 확인 기반을 종속 증명 검토의 중심에 두는 연구 도구 체인입니다.
- 산출물
- 원본 / 명세 / CI 템플릿
- 현재
- v0.1.1 공개 스냅샷
- 다음 검증
- 외부 정리 패키지와 독립 확인
실험
오픈소스
02
NPA 표준 라이브러리
Logic / Nat / List / Algebra
재사용 가능한 NPA 기초를 위한 표준 정리 패키지 저장소입니다.
- 산출물
- 원본 / 증명 패키지
- 현재
- 공개 분리 저장소
- 다음 검증
- 패키지 범위와 호환성
연구
오픈소스
03
NPA 수학 라이브러리
형식 수학 라이브러리
수학 정리를 독립적으로 확인 가능한 증명 패키지로 저장하기 위한 라이브러리 방향입니다.
- 산출물
- 원본 / 증명 패키지
- 현재
- 개발 중인 공개 저장소
- 다음 검증
- 라이브러리 구조와 의존성 감사
방법 검토
방법
04
제약 계획 모델
일정 / 경로 / 배정
교대, 방문, 경로, 생산, 배정 업무에서 필수 제약 조건과 평가 지표를 분리하는 방법입니다.
- 산출물
- 모델 / 프로토타입 / 설명 보고서
- 현재
- 서비스 방법이며 공개 주장은 방법 검토로 제한됩니다.
- 다음 검증
- 고객 증거와 범위 승인
연구
측정
05
재현 가능한 솔버 평가
벤치마크와 증거
성능을 주장하기 전에 인스턴스 세트, 하드웨어, 시간 제한, 난수 시드, 원시 로그를 고정하는 프로그램입니다.
- 산출물
- 벤치마크 등록부 / 원시 로그 / 보고서
- 현재
- 연구 프로그램 설계
- 다음 검증
- 첫 공개 벤치마크 말뭉치
연구
형식 기법
06
중요 업무 로직 검증
업무 시스템의 불변 조건
수수료, 권한, 재고, 상태 전이를 명세와 불변 조건으로 분리하는 연구입니다.
- 산출물
- 명세 / 불변 조건 / 테스트 또는 증명 보고서
- 현재
- 범위 검토
- 다음 검증
- 범위가 제한된 실제 생산 유사 사례 1개 선택
실험
엔지니어링
07
Rust의 작은 신뢰 컴포넌트
작은 신뢰 컴포넌트
검사기와 해시처럼 신뢰에 중요한 부분을 검사 가능한 크기로 유지하는 구현 작업입니다.
- 산출물
- NPA 커널 / 인증서 크레이트 / 참조 검사기
- 현재
- NPA의 공개 구현
- 다음 검증
- 독립 검사기 호환성
연구
AI × 증명
08
AI 보조와 독립 확인
자유롭게 생성하고 엄격하게 검증
AI는 후보 생성에 두고 최종 증거는 독립적으로 확인하는 연구 방향입니다.
- 산출물
- 후보 생성기 / 인증서 / 검사기 보고서
- 현재
- NPA 신뢰 모델과 일관된 연구 방향
- 다음 검증
- 측정 가능한 작성 흐름
조건에 맞는 연구 영역을 찾지 못했습니다.
다른 키워드를 시도하거나 성숙도 필터를 전체로 되돌려 보세요.
Nano Proof Auditor
증명 생성과 신뢰할 대상을 분리합니다.
NPA는 종속 증명을 위한 인증서 우선 증명 도구 체인입니다. 프런트엔드, 전술, 정리 검색, 플러그인, AI, 원본 파일, CI 상태는 후보 생성에 도움을 줄 수 있지만 신뢰할 증명 증거는 아닙니다.
실험오픈소스APACHE-2.0
현재 스냅샷
v0.1.1
공개 정보는 2026-06-21에 확인했습니다.
주요 코어
Rust
Rust 검증기와 커널은 확인 쪽에 포함됩니다.
감사 산출물
.npcert
표준 인증서 바이트가 검사 대상입니다.
재확인 지점
수동 검토
공개 전에 저장소 상태와 패키지 공개 범위를 검토해야 합니다.
신뢰 경계 탐색기
무엇을 신뢰하고 무엇을 신뢰하지 않는지 클릭해 확인하세요.
각 노드를 눌러 무엇을 하고, 무엇을 만들며, 어떤 확인이 여전히 필요한지 확인하세요.
비신뢰
확인됨
중요한 경계
현재 NPA는 Lean이나 Rocq의 실무적 대체물이 아닙니다. 이 페이지는 인증서 중심 연구 설계를 설명하며, 버그 없는 상용 시스템이나 자동 정리 증명을 보장하지 않습니다.
인증서 확인 / 설명용 시뮬레이션
인증서 확인 흐름을 확인해 보세요.
브라우저 상호작용은 검사 흐름을 설명합니다. NPA, Rust, WASM 또는 실제 증명 인증서를 실행하지 않습니다.
명령줄 예시
npa package verify-certs --root . --checker reference --json
NPA / 감사 추적
준비됨
- 01 인증서 읽기표준 바이트 / 형식 대기
- 02 인증서 해시 확인인증서 해시 대기
- 03 커널로 확인종속 증명 확인 대기
- 04 참조 검사기로 재확인원본 없는 판정 대기
- 05 공리 보고서 비교공리 보고서 해시 대기
판정
아직 설명을 실행하지 않았습니다.설명을 실행하면 단계가 순서대로 시각화됩니다.
증명 생태계
도구의 순위를 매기기보다 역할을 명확히 합니다.
Lean과 Rocq는 성숙한 증명 보조 도구 생태계입니다. NPA는 대체 순위가 아니라 인증서 중심의 연구 및 구현 프로젝트로 소개합니다.
| 항목 | Lean | Rocq | NPA |
|---|---|---|---|
| 위치 | 오픈소스 프로그래밍 언어이자 증명 보조 도구입니다. | 오랜 연구 역사를 가진 대화형 정리 증명기입니다. | 인증서 우선 확인을 위한 연구 및 구현 저장소입니다. |
| 주요 용도 | 수학, 소프트웨어 검증, 프로그래밍. | 수학, 명세, 프로그램 검증, 추출. | 증명 인증서와 독립 확인에 관한 연구. |
| 중점 | 확장성, 라이브러리, 대화형 증명. | 표현력, 성숙한 방법론, 라이브러리. | 작은 신뢰 기반과 표준 인증서. |
| 이 페이지의 취급 방식 | 학습, 비교, 상호 운용성을 위한 참고 기준입니다. | 학습, 비교, 형식화 방법을 위한 참고 기준입니다. | Finite Field의 연구 프로젝트입니다. |
| 경계 | 전문 지식은 여전히 필요합니다. | 전문 지식은 여전히 필요합니다. | 현재 Lean이나 Rocq의 실무적 대체물을 의도하지 않습니다. |
연구 방법
“작동했다”를 반복 가능한 확인 절차로 바꿉니다.
누군가 같은 조건에서 다시 실행하고, 검사하고, 거부할 수 있을 때 결과는 더 강해집니다.
질문
성능, 정확성, 호환성, 범위 중 무엇을 확인할지 정의합니다.
가정
평가 전에 가정, 제외 사항, 공리, 데이터 공백, 편향을 적습니다.
산출물
원본, 인증서, 입력, 실행 로그, 해시를 남깁니다.
독립 확인
생성 쪽과 다른 경로로 결과를 확인합니다.
벤치마크
하드웨어, 버전, 시간 제한, 인스턴스 세트, 난수 시드를 고정합니다.
한계
실패, 미지원 사례, 성능 경계, 다음 검증을 공개합니다.
재현성 빌더
연구 공개에 아직 부족한 점을 확인합니다.
체크리스트는 브라우저 안에서만 처리됩니다. 인증 점수가 아닙니다.
준비도
0%다음 행동
먼저 연구 질문과 성공 조건을 정의하세요.산출물 형식을 정하기 전에 무엇을 비교하거나 확인할지 고정합니다.
공개 산출물
공개 산출물을 한 곳에서 추적합니다.
이 페이지는 실행 중 GitHub API를 호출하지 않습니다. 저장소 상태는 공개 전 검토가 필요한 확인된 스냅샷입니다.
4 개 산출물
finitefield-org
npa
인증서 우선 증명 도구 체인
확인
package verify-certs
finitefield-org
npa-std
표준 정리 패키지
역할
Std.Logic / Nat / List
finitefield-org
npa-mathlib
형식 수학 라이브러리
역할
형식 정리 패키지
GitHub
finitefield-org
공개 저장소 색인
색인
전체 공개 저장소
검색 조건에 맞는 공개 산출물이 없습니다.
공개 정책
공개 저장소, 연구 노트, 벤치마크에는 확인 날짜, 성숙도, 재현 단계, 알려진 한계가 있어야 합니다. 별 수나 커밋 수는 연구 품질 신호로 표시하지 않습니다.
랩에서 운영으로
연구의 엄밀함을 업무 시스템 설계에 가져옵니다.
모든 고객 시스템에 정리 증명이 필요한 것은 아닙니다. 중요한 것은 무엇을 신뢰하고, 비교하고, 확인하고, 수정하고, 사람이 승인해야 하는지 정하는 일입니다.
랩의 실천 방식
모든 계층을 똑같이 신뢰하지 않고 생성, 계산, 최종 확인을 분리합니다.
입력, 출력, 인증서, 해시, 로그를 검토 가능한 산출물로 남깁니다.
결과를 비교하기 전에 데이터, 버전, 명령, 평가 기준을 고정합니다.
제약 조건, 실패 사례, 미해결 사항을 결과와 같은 비중으로 공개합니다.
고객 시스템
누가 입력하고, 검토하고, 덮어쓰고, 결과를 확정하는지 정의합니다.
제약 조건, 평가 점수, 탈락한 후보, 미해결 사항을 보여줍니다.
조건 변경, 계산 실행, 최종 승인 이력을 보존합니다.
자동 출력은 운영자가 수정하고, 거부하고, 설명할 수 있게 만듭니다.
연구 노트
업데이트 이력과 증거를 읽기 쉽게 유지합니다.
모든 카드가 공개 글은 아닙니다. 준비 중인 노트는 날짜, 출처, 재현 단계가 갖춰질 때까지 공개 작업으로 표시하지 않습니다.
NPA / 현재
인증서를 중심에 두는 이유
최종 증거가 작은 독립 경로에서 확인되는 표준 인증서여야 하는 이유입니다.
공개 저장소 보기설계 노트 / 예정
최적화 결과를 설명 가능하게 만들기
목적, 필수 제약 조건, 선호 조건, 미해결 배정을 화면에 드러내는 설계 노트입니다.
관련 데모 보기벤치마크 / 예정
공정한 솔버 비교를 위한 조건
인스턴스 세트, 시간 제한, 최적성 격차, 난수 시드, 하드웨어에 관한 예정 노트입니다.
공개 기준 보기“준비 중” 항목은 공개 글이 아닙니다. 공개 후 각 노트에는 날짜, 출처, 작성자, 재현 경로, 알려진 한계가 붙습니다.
01 수학 랩은 계약 개발 서비스인가요?
아니요. 연구 태도와 산출물을 공개하는 공간입니다. 고객 논의에서는 적용 가능한 방법, 추가 검증이 필요한 방법, 연구 단계 주제를 구분합니다.
02 NPA가 Lean이나 Rocq를 대체할 수 있나요?
아니요. 현재 NPA는 Lean이나 Rocq의 실무적 대체물이 아닙니다. 인증서, 독립 확인, 작은 신뢰 기반을 다루는 연구 및 구현 프로젝트입니다.
03 AI가 생성한 증명을 그대로 신뢰하나요?
아니요. AI, 검색, 전술은 후보 생성에 도움을 줍니다. 우리는 최종 인증서가 생성 경로와 독립적인 검사기에서 승인되는지에 집중합니다.
04 형식 검증이 모든 버그를 없애나요?
아니요. 형식 기법은 명시적 명세에 대한 특정 속성을 확인합니다. 잘못된 명세, 범위 밖 코드, 운영, 외부 서비스는 별도 검토가 필요합니다.
05 이 내용이 업무 시스템 작업과 관련되나요?
네. 보통 제약 조건, 결과 사유, 계산 이력, 권한 경계, 중요한 업무 로직 확인부터 단계적으로 적용합니다.
출처 스냅샷 / 2026-06-21
NPA 관련 주장은 finitefield-org/npa 저장소 스냅샷을 기준으로 합니다. Lean과 Rocq의 위치 설명은 각 공식 사이트를 기준으로 합니다. 저장소 상태, 최신 태그, 방법 검토 문구는 2026-06-28에 확인했습니다.