NPA / சான்றிதழ்-முதன்மை proof checking

NPA: முடிவை நம்புவதற்கு முன் சான்று ஆதார எல்லையை வெளிப்படுத்துங்கள்.

இந்தப் பக்கம் Math Lab-இன் NPA பிரிவை தனித்த ஆதாரப் பக்கமாக மறுவடிவமைக்கிறது: பொது நிலை, trust model, proof pipeline, கூற்று பதிவேடு, repositories, sources, மற்றும் மாற்றாக அல்ல என்ற தெளிவான மொழி.

trust boundary-ஐ ஆய்வு செய் GitHub repository-ஐ திற

பொது நிலை: ஆராய்ச்சி repository; production assurance service ஆக அல்ல, ஆராய்ச்சி மற்றும் செயலாக்கமாகக் காட்டப்படுகிறது.
பொது மறுபரிசோதனை: 2026-07-02 / NPA v0.2.0; சரிபார்க்கப்பட்ட latest git tags: npa v0.2.0, npa-std v0.1.0, npa-mathlib v0.1.30.
உரிமம்: Apache-2.0; npa, npa-std, npa-mathlib க்கு Apache-2.0 2026-07-02 அன்று சரிபார்க்கப்பட்டது.

பொது மறுசரிபார்ப்பு: 2026-07-02. NPA repository latest git tag v0.2.0; npa-std v0.1.0; npa-mathlib v0.1.30. Package README pins repository-சார் context ஆகக் காட்டப்படுகின்றன; ஒரே NPA version claim ஆகச் சுருக்கப்படவில்லை.

சான்றிதழ் சரிபார்ப்பு மற்றும் trust-boundary ஆய்வைக் காட்டும் NPA evidence page preview — இந்த visual சான்றிதழ் சரிபார்ப்பு முடிவும் trust-boundary விளக்கமும் கொண்ட static preview. இது live NPA trace அல்ல.

பொது நிலை

எது பொதுவானது, எது ஆதாரம், எப்போது மீண்டும் சரிபார்க்கப்பட்டது என்பதைத் தெளிவுபடுத்துங்கள்.

இந்தப் பக்கத்தின் அடிப்படை தெளிவாக காட்டப்படுகிறது: உள்ளூர் உண்மை snapshot, பொது repository source, இறுதி prelaunch readback date.

பொது நிலை

ஆராய்ச்சி மற்றும் செயலாக்க repository

GitHub repository பொது நிலையில் உள்ளது; ஆனால் இந்தப் பக்கம் deployed service அல்ல, ஆராய்ச்சி மற்றும் செயலாக்க repository-யை விவரிக்கிறது.

பொது மறுபரிசோதனை

2026-07-02

public-source readback 2026-07-02 அன்று முடிந்தது. அசல் source reconstruction இன்னும் 2026-06-21 local truth snapshot-ஐப் பயன்படுத்துகிறது.

ஆதாரம்

சான்றிதழ்கள் மற்றும் hashes

source snapshot canonical .npcert, certificate_hash, export_hash, axiom_report_hash, checker verdicts ஆகியவற்றைப் பதிவு செய்கிறது.

உரிமம்

Apache-2.0 சரிபார்க்கப்பட்டது

npa, npa-std, npa-mathlib க்கு Apache-2.0 பொது LICENSE metadata வழியாக 2026-07-02 அன்று சரிபார்க்கப்பட்டது.

எல்லை

NPA Lean அல்லது Rocq-க்கு நடைமுறை மாற்றாக இல்லை. பகிரப்பட்ட browser inspection simulation NPA தானாக இயக்காது. final publication readback-க்காக public tags, license, repository visibility 2026-07-02 அன்று சரிபார்க்கப்பட்டன.

Trust boundary

சான்று ஆதார எல்லையை canonical certificate மட்டும் கடக்கட்டும்.

எந்த கருவி நவீனமாகத் தோன்றுகிறது என்பதே எல்லை அல்ல. சுயாதீன சரிபார்ப்புக்குப் பிறகு எந்த ஆதாரப் பொருள் evidence ஆக அனுமதிக்கப்படுகிறது என்பதே முக்கியம்.

Parser, elaborator, tactics, automation, theorem search, plugins, AI systems, source files, replay files, theorem indexes, publish plans, CI status, release pages, registry metadata ஆகியவை untrusted candidate side-இல் இருக்கும்.

Proof pipeline / விளக்க simulation

certificate bytes-இலிருந்து checking evidence வரை உள்ள சரியான pipeline-ஐக் காட்டுங்கள்.

உலாவி simulation NPA தானாகவோ, Rust, WASM அல்லது உண்மையான proof certificates-ஐயோ இயக்காது. உண்மையான artifacts பூர்த்தி செய்ய வேண்டிய source-free checking வரிசையை அது காட்சிப்படுத்துகிறது.

CLI ஆதார பாதை

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

NPA / audit trace தயார்

01 Certificate formatcanonical .npcert bytes / parse செய்யக்கூடிய certificate / format சரிபார்ப்பு காத்திரு
02 Certificate hashcertificate bytes / certificate_hash / deterministic digest காத்திரு
03 Kernel verdictcertificate / accept அல்லது reject / Rust verifier report காத்திரு
04 Reference checkerhash-pinned certificate / independent accept அல்லது reject / source-free checker report காத்திரு
05 Axiom reportசரிபார்க்கப்பட்ட package / axiom_report_hash / assumption பட்டியல் காத்திரு

தீர்ப்பு

விளக்க pipeline இன்னும் இயக்கப்படவில்லை.

source-free checking பாதையை வரிசையாகக் குறிக்க விளக்கத்தை இயக்குங்கள்.

கூற்று பதிவேடு

ஆதாரம், கால உணர்வு கொண்ட உண்மைகள், எல்லைக் கூற்றுகள் ஆகியவற்றைப் பிரிக்கவும்.

இந்தப் பக்கம் தெளிவற்ற ஆராய்ச்சி உரையை சார்ந்ததல்ல. ஒவ்வொரு பொது கூற்றும் உள்ளூர் உண்மை snapshot, ஒரு மூலம், ஒரு வெளியீட்டு நடவடிக்கை ஆகியவற்றுடன் இணைக்கப்பட்டுள்ளது.

கூற்று	பொது சொற்கள்	நிலை	மூலம்	வெளியீட்டு நடவடிக்கை
CL-001	NPA சான்றிதழ்-முதன்மை அணுகுமுறை கொண்டது: தணிக்கைக்குரிய எல்லை canonical .npcert ஆதாரப் பொருளும் அதைச் சுற்றிய சரிபார்ப்பு பாதையும் ஆகும்.	சரிபார்க்கப்பட்ட பொது கூற்று	S01 / 2026-07-02	README மாறும்போது மீண்டும் மதிப்பாய்வு செய்யவும்.
CL-002	2026-07-02 பொது மறுசரிபார்ப்பில் NPA repository latest git tag v0.2.0 என உறுதி செய்யப்பட்டது. தொடர்புடைய package README-கள் repository-சார் pins-ஐ காட்டுவதால், பதிப்பு சொற்கள் repository வரம்புக்குள் வைக்கப்படுகின்றன.	சரிபார்க்கப்பட்ட பொது மறுசரிபார்ப்பு	S01 / S02 / 2026-07-02	tag சொற்களை repository வரம்புக்குள் வைத்திருங்கள்.
CL-003	உள்ளூர் உண்மை snapshot Rust 1.95.0 toolchain pin-ஐ பதிவு செய்கிறது; அது marketing கூற்றாக பயன்படுத்தப்படவில்லை.	சரிபார்க்கப்பட்டது, கால உணர்வு கொண்டது	S01 / 2026-07-02	toolchain பதிப்பு காட்டப்படும் போது மீண்டும் சரிபார்க்கவும்.
CL-004	NPA, Lean அல்லது Rocq-க்கு நடைமுறை மாற்றாக இல்லை. எந்த ஒப்பீட்டின் அருகிலும் இந்த எல்லை தெளிவாகத் தெரிய வேண்டும்.	சரிபார்க்கப்பட்ட எல்லைக் கூற்று	S01 / S03 / S05 / 2026-07-02	disclaimer-ஐ வைத்திருக்கவும்.
CL-005	npa-std மற்றும் npa-mathlib finitefield-org அமைப்பில் உள்ள தனித்தனி பொது theorem-package repositories ஆகும்.	சரிபார்க்கப்பட்ட பொது கூற்று	S01 / S02 / 2026-07-02	வெளியீடு தாமதமானாலோ repositories மாறினாலோ repository காட்சியளிப்பை மீண்டும் சரிபார்க்கவும்.
CL-006	npa, npa-std, npa-mathlib repositories ஒவ்வொன்றும் தங்களின் பொது LICENSE metadata வழியாக Apache-2.0 உரிமத்தை வெளிப்படுத்துகின்றன.	சரிபார்க்கப்பட்ட பொது கூற்று	S01 / S02 / 2026-07-02	major release-இல் LICENSE-ஐ மீண்டும் சரிபார்க்கவும்.

Repositories மற்றும் உரிமம்

code, package repositories, organization visibility ஆகியவற்றை வெளிப்படையாக வைத்திருங்கள்.

Repository links public-source pointers மட்டுமே; தற்போதைய பக்கம் latest GitHub state-உடன் ஒத்திசைக்கப்பட்டுள்ளது என்ற உத்தரவாதம் அல்ல.

4 repositories காட்டப்பட்டன

finitefield-org

npa

Certificate-first proof assistance மற்றும் verification toolchain.

உரிமம்: Apache-2.0 2026-07-02 அன்று LICENSE-இல் இருந்து சரிபார்க்கப்பட்டது.
சரிபார்ப்பு: Latest git tag: v0.2.0. latest GitHub release வெளியிடப்படவில்லை. README தற்போதைய toolchain reference: NPA_GIT_TAG=v0.2.0.

சோதனை நிலைRust / OCamlcertificate-first

repository-ஐ திற

finitefield-org

npa-std

NPA proof sources-க்கான standard theorem package repository.

உரிமம்: Apache-2.0 2026-07-02 அன்று LICENSE-இல் இருந்து சரிபார்க்கப்பட்டது.
சரிபார்ப்பு: Latest git tag மற்றும் GitHub release: v0.1.0. README package metadata version: 0.1.0; package toolchain pin: NPA_GIT_TAG=v0.1.1.

சோதனை நிலைtheorem packageproof source

repository-ஐ திற

finitefield-org

npa-mathlib

Formal mathematics library research repository.

உரிமம்: Apache-2.0 2026-07-02 அன்று LICENSE-இல் இருந்து சரிபார்க்கப்பட்டது.
சரிபார்ப்பு: Latest git tag: v0.1.30. Latest GitHub release: v0.1.9. README package metadata version: 0.2.1; package toolchain pin: NPA_GIT_TAG=v0.1.1.

ஆராய்ச்சிformal mathematicslibrary

repository-ஐ திற

finitefield-org

Finite Field GitHub organization

Lab repository family-க்கான public organization snapshot.

உரிமம்: repository-சார் licenses பொருந்தும்
சரிபார்ப்பு: 2026-07-02 GitHub API readback படி npa, npa-std, npa-mathlib பொது repositories ஆக உள்ளன.

public indexvisibility snapshotsource

organization-ஐ திற

GitHub repositories public code status-க்கான source ஆகும். License, current tags, public visibility, release wording ஆகியவை M10-T14 final readback ஆக 2026-07-02 அன்று சரிபார்க்கப்பட்டன.

சான்று சூழல் guard

சான்று கருவிகளை ஒப்பிடுவதற்கு முன் பங்குகளைத் தெளிவுபடுத்துங்கள்.

இது தரவரிசை அல்ல, பங்கு அட்டவணை. Lean மற்றும் Rocq சான்று உதவி சூழல்களுக்கான reference ஆகவே உள்ளன; NPA சான்றிதழ் மையமான ஆராய்ச்சி மற்றும் செயலாக்கப் பணியாகக் காட்டப்படுகிறது.

உருப்படி	Lean	Rocq	NPA
நிலைப்பாடு	திறந்த மூல நிரல்மொழியும் சான்று உதவியும்.	நீண்ட ஆராய்ச்சி வரலாற்றைக் கொண்ட தொடர்பாடல் தேற்றச் சான்றுபடுத்தி.	சான்றிதழ்-முதன்மை சரிபார்ப்புக்கான ஆராய்ச்சி மற்றும் செயலாக்க repository.
வழக்கமான பயன்பாடு	கணிதம், மென்பொருள் சரிபார்ப்பு, நிரலாக்கம்.	கணிதம், விவரக்குறிப்புகள், நிரல் சரிபார்ப்பு, பிரித்தெடுப்பு.	proof certificates, சுயாதீன சரிபார்ப்பு, சிறிய trusted base குறித்த ஆராய்ச்சி.
சான்று எல்லை	அதன் சொந்த நம்பத்தகுந்த கர்னலும் சூழலும் சரிபார்ப்பு எல்லையை வரையறுக்கின்றன.	அதன் சொந்த கர்னலும் சரிபார்க்கப்பட்ட developments-உம் சரிபார்ப்பு எல்லையை வரையறுக்கின்றன.	canonical .npcert ஆதாரப் பொருள் உருவாக்கத்திலிருந்து சரிபார்ப்புக்குள் கடக்கிறது.
இந்தப் பக்கம் அதை அணுகும் விதம்	கற்றல், ஒப்பீடு, பரஸ்பர இயங்குதன்மைக்கான குறிப்பு.	கற்றல், ஒப்பீடு, வடிவமுறைப்படுத்தல் முறைகளுக்கான குறிப்பு.	Finite Field ஆராய்ச்சி திட்டம்; தயாரிப்பு வாக்குறுதி அல்ல.
எல்லை	சிறப்பு அறிவு இன்னும் தேவைப்படுகிறது.	சிறப்பு அறிவு இன்னும் தேவைப்படுகிறது.	இந்த நேரத்தில் NPA, Lean அல்லது Rocq-க்கு நடைமுறை மாற்றாக இல்லை.

Lean அதிகாரப்பூர்வ தளம் Rocq அதிகாரப்பூர்வ தளம் NPA GitHub

மூலங்கள்

விளக்கத்தின் அருகில் source map-ஐ வெளியிடுங்கள்.

எந்த கூற்றுகள் public repositories, official proof-tool sites, company context ஆகியவற்றிலிருந்து வருகின்றன என்பதை வாசகர் அறிய sources காட்டப்படுகின்றன.

S01

finitefield-org/npa

NPA நோக்கம், trust model, v0.2.0 current repository tag wording, commands, repository layout, license ஆகியவற்றுக்கான முதன்மை மூலம்.

மூலத்தைத் திற S02

Finite Field GitHub organization

public repository visibility, latest git tags, release pages, 2026-07-02 அன்று சரிபார்க்கப்பட்ட Lab repository family snapshot ஆகியவற்றுக்கான முதன்மை மூலம்.

மூலத்தைத் திற S03

Lean அதிகாரப்பூர்வ தளம்

Lean பொது positioning-க்கான முதன்மை மூலம்; 2026-07-02 அன்று சரிபார்க்கப்பட்டது.

மூலத்தைத் திற S04

Lean language reference

dependent type theory மற்றும் kernel reference context-க்கான முதன்மை மூலம்; 2026-07-02 அன்று சரிபார்க்கப்பட்டது.

மூலத்தைத் திற S05

Rocq அதிகாரப்பூர்வ தளம்

Rocq பொது positioning-க்கான முதன்மை மூலம்; 2026-07-02 அன்று சரிபார்க்கப்பட்டது.

மூலத்தைத் திற S06

FINITE FIELD நிறுவனத் தளம்

Finite Field brand மற்றும் business context-க்கான company source.

மூலத்தைத் திற

FAQ

NPA நிலை மற்றும் verification எல்லைகள்.

ஆராய்ச்சி பக்கத்தை செயல்பாட்டில் உள்ள proof-assistant சேவையாக வாசகர்கள் தவறாகக் கருதுவதற்கு முன், பதில்கள் trust boundary-ஐ வலியுறுத்துகின்றன.

நிறுவனம் பற்றி வாசிக்கவும்

01 இந்தப் பக்கம் product guarantee ஆகுமா?

இல்லை. NPA இங்கு ஆராய்ச்சி மற்றும் செயலாக்க repository ஆகக் காட்டப்படுகிறது.

02 NPA Lean அல்லது Rocq-ஐ மாற்றுமா?

இல்லை. NPA Lean அல்லது Rocq-க்கு நடைமுறை மாற்றாக இல்லை.

03 இந்தப் பக்கம் உண்மையான NPA verification-ஐ இயக்குகிறதா?

இல்லை. உலாவி simulation NPA தானாகவோ, Rust, WASM அல்லது உண்மையான proof certificates-ஐயோ இயக்காது.

04 இங்கு எது ஆதாரமாகக் கருதப்படுகிறது?

certificate artifact, deterministic hashes, Rust kernel/verifier முடிவு, source-free reference checker முடிவு, axiom report ஆகியவை checking-side evidence ஆகின்றன.

05 எந்த உண்மைகள் மீண்டும் சரிபார்க்கப்பட வேண்டும்?

தற்போதைய பொது பதிப்பு, repository காட்சியளிப்பு, toolchain pins, license உரை, source சொற்கள் 2026-07-02 அன்று மீண்டும் சரிபார்க்கப்பட்டன.

சான்று ஒழுங்கிலிருந்து செயல்பாட்டுக்கு

வணிக முடிவை நம்ப வேண்டிய இடங்களில் இதே ஆதார ஒழுங்கைப் பயன்படுத்துங்கள்.

வணிக அமைப்புகளுக்கு பயனுள்ள பாடம் எல்லா இடங்களிலும் தேற்றச் சான்றிடலைச் சேர்ப்பது அல்ல. எதை உருவாக்க வேண்டும், சரிபார்க்க வேண்டும், பதிவு செய்ய வேண்டும், திருத்த வேண்டும், மனிதர்கள் ஒப்புதல் அளிக்க வேண்டும் என்பதை முடிவு செய்வதே முக்கியம்.

வணிகச் சிக்கலைச் சரிபார்க்கவும் முன்மாதிரியைப் பார்க்கவும்