NPA / בדיקת הוכחות שמתחילה מתעודות

NPA: הציגו את גבול ראיות ההוכחה לפני שנותנים אמון בתוצאה.

הדף הזה משחזר את אזור NPA ממעבדת המתמטיקה כדף ראיות עצמאי: מצב ציבורי, מודל אמון, צינור הוכחה, מרשם טענות, מאגרים, מקורות וניסוח מפורש שאינו מציג אותה כתחליף.

בדיקת גבול האמון פתיחת מאגר GitHub

מצב ציבורי: מאגר מחקר; מוצג כמחקר ויישום, לא כשירות אבטחת ייצור.
בדיקה ציבורית חוזרת: 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. קיבועי README של חבילות מוצגים כהקשר ייעודי למאגר ואינם משוטחים לטענת גרסה אחת של NPA.

תצוגה מקדימה של דף ראיות NPA המציגה בדיקת תעודות ובחינת גבול אמון — האיור הוא תצוגה מקדימה סטטית של תוצאת בדיקת התעודות והסבר גבול האמון. הוא אינו עקבת NPA חיה.

מצב ציבורי

ציינו מה ציבורי, מה נחשב ראיה ומתי נבדק מחדש.

הדף מציג במפורש את בסיסו: תמונת אמת מקומית, מקור מאגר ציבורי ותאריך הקריאה החוזרת הסופית לפני השקה.

מצב ציבורי

מאגר מחקר ויישום

מאגר GitHub ציבורי, אך הדף הזה מתאר מאגר מחקר ויישום, לא שירות פרוס.

בדיקה ציבורית חוזרת

2026-07-02

קריאת המקורות הציבוריים הושלמה ב-2026-07-02. שחזור המקור המקורי עדיין משתמש בתמונת האמת המקומית מ-2026-06-21.

ראיות

תעודות וגיבובים

תמונת המקור מתעדת .npcert קנוני, certificate_hash, export_hash, axiom_report_hash ופסקי בודק.

רישיון

Apache-2.0 אומת

Apache-2.0 אומת עבור npa, npa-std ו-npa-mathlib דרך מטא-נתוני LICENSE ציבוריים ב-2026-07-02.

גבול

NPA אינה תחליף מעשי ל-Lean או Rocq. סימולציית הבדיקה שמופצת בדפדפן אינה מריצה את NPA עצמה. תגים ציבוריים, רישיון ונראות מאגרים נבדקו ב-2026-07-02 לקראת קריאת הפרסום הסופית.

גבול אמון

העבירו רק תעודה קנונית מעבר לגבול הראיות.

הגבול אינו עוסק בשאלה איזה כלי נראה מתוחכם. הוא עוסק בשאלה איזה ממצא רשאי להפוך לראיה לאחר בדיקה עצמאית.

מנתח, מרחיב, טקטיקות, אוטומציה, חיפוש משפטים, תוספים, מערכות בינה מלאכותית, קובצי מקור, קובצי הרצה חוזרת, אינדקסי משפטים, תוכניות פרסום, סטטוס CI, דפי גרסאות ומטא-נתוני מרשם נשארים בצד המועמדים הלא מהימן.

צינור הוכחה / סימולציה מסבירה

הציגו את הצינור המדויק מבתי התעודה ועד ראיות הבדיקה.

סימולציית הדפדפן אינה מריצה את 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 מתחילה מתעודות: גבול הביקורת הוא ממצא .npcert קנוני ומסלול הבדיקה שסביבו.	טענה ציבורית מאומתת	S01 / 2026-07-02	לבדוק מחדש כאשר ה-README משתנה.
CL-002	בבדיקה הציבורית החוזרת מ-2026-07-02 נמצא שהתג האחרון במאגר NPA הוא v0.2.0. קובצי README של חבילות קשורות עדיין מציגים קיבועי גרסה ייעודיים למאגר, לכן נוסח הגרסאות נשאר מוגבל לכל מאגר בנפרד.	בדיקה ציבורית חוזרת מאומתת	S01 / S02 / 2026-07-02	להשאיר את ניסוח התגים מוגבל לכל מאגר.
CL-003	תמונת האמת המקומית מתעדת קיבוע שרשרת כלים Rust 1.95.0; אין להשתמש בכך כטענה שיווקית.	מאומת, תלוי זמן	S01 / 2026-07-02	לבדוק מחדש אם גרסת שרשרת הכלים מוצגת.
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 דרך מטא-נתוני LICENSE הציבוריים שלהם.	טענה ציבורית מאומתת	S01 / S02 / 2026-07-02	לבדוק מחדש את LICENSE בעת גרסה משמעותית.

מאגרים ורישיון

הקפידו שהקוד, מאגרי החבילות ונראות הארגון יהיו מפורשים.

קישורי המאגרים הם הפניות למקור ציבורי, לא הבטחה שהדף הנוכחי מסונכרן עם מצב GitHub האחרון.

4 מאגרים מוצגים

finitefield-org

npa

שרשרת כלי סיוע ואימות להוכחות שמתחילה מתעודות.

רישיון: Apache-2.0 אומת מתוך LICENSE ב-2026-07-02.
אימות: תג git אחרון: v0.2.0. לא פורסמה גרסת GitHub אחרונה. הפניית שרשרת הכלים הנוכחית ב-README: NPA_GIT_TAG=v0.2.0.

ניסיוניRust / OCamlמתחיל מתעודות

פתיחת מאגר

finitefield-org

npa-std

מאגר חבילות משפטים סטנדרטי עבור מקורות הוכחה של NPA.

רישיון: Apache-2.0 אומת מתוך LICENSE ב-2026-07-02.
אימות: תג git וגרסת GitHub אחרונים: v0.1.0. גרסת מטא-נתוני החבילה ב-README: 0.1.0; קיבוע שרשרת הכלים של החבילה: NPA_GIT_TAG=v0.1.1.

ניסיוניחבילת משפטיםמקור הוכחה

פתיחת מאגר

finitefield-org

npa-mathlib

מאגר מחקר לספריית מתמטיקה פורמלית.

רישיון: Apache-2.0 אומת מתוך LICENSE ב-2026-07-02.
אימות: תג git אחרון: v0.1.30. גרסת GitHub אחרונה: v0.1.9. גרסת מטא-נתוני החבילה ב-README: 0.2.1; קיבוע שרשרת הכלים של החבילה: NPA_GIT_TAG=v0.1.1.

מחקרמתמטיקה פורמליתספרייה

פתיחת מאגר

finitefield-org

ארגון GitHub של Finite Field

תמונת מצב ציבורית של הארגון עבור משפחת מאגרי המעבדה.

רישיון: חלים רישיונות ייעודיים לכל מאגר
אימות: npa, npa-std ו-npa-mathlib ציבוריים לפי קריאת GitHub API חוזרת מ-2026-07-02.

אינדקס ציבוריתמונת נראותמקור

פתיחת הארגון

מאגרי GitHub הם המקור למצב הקוד הציבורי. רישיון, תגים נוכחיים, נראות ציבורית ונוסח גרסאות נבדקו ב-2026-07-02 כחלק מקריאת הסיום של M10-T14.

גבול אקוסיסטם ההוכחות

הבהירו תפקידים לפני שמשווים כלי הוכחה.

זו טבלת תפקידים, לא דירוג. Lean ו-Rocq נשארות אקוסיסטמי הייחוס לעוזרי הוכחה; NPA מוצגת כעבודת מחקר ויישום שממוקדת בתעודות.

פריט	Lean	Rocq	NPA
מיקום	שפת תכנות ועוזר הוכחה בקוד פתוח.	מוכיח משפטים אינטראקטיבי עם היסטוריה מחקרית ארוכה.	מאגר מחקר ויישום לבדיקה שמתחילה מתעודות.
שימוש טיפוסי	מתמטיקה, אימות תוכנה ותכנות.	מתמטיקה, מפרטים, אימות תוכניות וחילוץ.	מחקר בתעודות הוכחה, בדיקה עצמאית ובסיס אמון קטן.
גבול ראיות	הליבה המהימנה והאקוסיסטם שלה מגדירים את גבול הבדיקה.	הליבה שלה ופיתוחים שנבדקו מגדירים את גבול הבדיקה.	ממצא .npcert קנוני עובר משלב היצירה לשלב הבדיקה.
איך הדף מתייחס לכך	נקודת ייחוס ללמידה, להשוואה ולתאימות.	נקודת ייחוס ללמידה, להשוואה ולשיטות פורמליזציה.	פרויקט מחקר של Finite Field, לא הבטחת מוצר.
גבול	עדיין נדרש ידע מומחה.	עדיין נדרש ידע מומחה.	בשלב זה NPA אינה תחליף מעשי ל-Lean או Rocq.

האתר הרשמי של Lean האתר הרשמי של Rocq Prover NPA ב-GitHub

מקורות

פרסמו את מפת המקורות לצד הפרשנות.

המקורות מוצגים כדי שהקורא יוכל לדעת אילו טענות מגיעות ממאגרים ציבוריים, מאתרים רשמיים של כלי הוכחה ומהקשר החברה.

S01

finitefield-org/npa

מקור ראשי למטרת NPA, מודל האמון, נוסח תג המאגר הנוכחי v0.2.0, פקודות, מבנה המאגר ורישיון.

פתיחת מקור S02

ארגון GitHub של Finite Field

מקור ראשי לנראות מאגרים ציבוריים, תגי git אחרונים, דפי גרסאות ותמונת מצב של משפחת מאגרי המעבדה שנבדקה ב-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 ולהקשר העסקי.

פתיחת מקור

שאלות נפוצות

מעמד NPA וגבולות האימות.

התשובות מדגישות את גבול האמון לפני שקוראים יבלבלו בין דף מחקר לבין שירות עוזר הוכחה פרוס.

קריאה על החברה

01 האם הדף הזה הוא הבטחת מוצר?

לא. NPA מוצגת כאן כמאגר מחקר ויישום.

02 האם NPA יכולה להחליף את Lean או Rocq?

לא. NPA אינה תחליף מעשי ל-Lean או Rocq.

03 האם הדף מריץ אימות NPA אמיתי?

לא. סימולציית הדפדפן אינה מריצה את NPA עצמה, Rust, WASM או תעודות הוכחה אמיתיות.

04 מה נחשב כאן ראיה?

ממצא התעודה, גיבובים דטרמיניסטיים, תוצאת ליבת/מאמת Rust, תוצאת בודק ייחוס ללא מקור ודוח האקסיומות הם הראיות מצד הבדיקה.

05 אילו עובדות דורשות בדיקה חוזרת?

הגרסה הציבורית הנוכחית, נראות המאגרים, קיבועי שרשרת הכלים, נוסח הרישיון וניסוח המקורות נבדקו מחדש ב-2026-07-02.

ממשמעת הוכחה לתפעול

השתמשו באותה משמעת ראיות כאשר צריך לבטוח בהחלטה עסקית.

במערכות עסקיות, הלקח השימושי אינו להוסיף הוכחת משפטים לכל מקום. הלקח הוא להחליט מה צריך ליצור, לבדוק, לתעד, לתקן ולאשר בידי אנשים.

בדיקת הסוגיה העסקית צפייה באבטיפוס