01 / גבול
שמרו על בסיס אמון קטן
אל תמקמו מחוללים מורכבים או בינה מלאכותית במרכז האמון. הפכו את צד הבדיקה הקטן למפורש.
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
לוגיקה / טבעיים / רשימות / אלגברה
מאגר חבילות משפטים סטנדרטי עבור יסודות NPA לשימוש חוזר.
- ממצאים
- מקור / חבילות הוכחה
- נוכחי
- מאגר ציבורי מפוצל
- האימות הבא
- היקף חבילה ותאימות
מחקר
קוד פתוח
03
ספריית המתמטיקה של NPA
ספרייה למתמטיקה פורמלית
כיוון ספרייתי לשמירת משפטים מתמטיים כחבילות הוכחה שניתנות לבדיקה עצמאית.
- ממצאים
- מקור / חבילות הוכחה
- נוכחי
- מאגר ציבורי בפיתוח
- האימות הבא
- מבנה ספרייה וביקורת תלויות
סקירת שיטה
שיטה
04
מודלים לתכנון עם אילוצים
תזמון / ניתוב / הקצאה
שיטה להפרדת אילוצים קשיחים ומדדי הערכה בעבודות משמרות, ביקורים, ניתוב, ייצור והקצאה.
- ממצאים
- מודל / אבטיפוס / דוח הסבר
- נוכחי
- שיטת שירות; הטענה הציבורית מוגבלת לסקירת שיטה
- האימות הבא
- ראיות לקוח ואישור היקף
מחקר
מדידה
05
הערכת פותרים שניתנת לשחזור
מדדי השוואה וראיות
תוכנית לקיבוע קבוצות מקרים, חומרה, מגבלות זמן, זרעים אקראיים ולוגים גולמיים לפני טענות ביצועים.
- ממצאים
- מרשם מדדי השוואה / לוגים גולמיים / דוח
- נוכחי
- תכנון תוכנית מחקר
- האימות הבא
- קורפוס מדדי השוואה ציבורי ראשון
מחקר
שיטות פורמליות
06
אימות ללוגיקה עסקית קריטית
אינווריאנטים למערכות עסקיות
מחקר על הפרדת עמלות, הרשאות, מלאי ומעברי מצב למפרטים ולאינווריאנטים.
- ממצאים
- מפרט / אינווריאנטים / דוח בדיקה או הוכחה
- נוכחי
- בדיקת היקף
- האימות הבא
- בחירת מקרה מוגבל אחד הדומה לייצור
ניסיוני
הנדסה
07
רכיבי אמון קטנים ב-Rust
רכיבי אמון קטנים
עבודת יישום ששומרת רכיבים קריטיים לאמון, כגון בודקים וגיבובים, קטנים מספיק לבדיקה.
- ממצאים
- ליבת NPA / crate תעודות / בודק ייחוס
- נוכחי
- יישום ציבורי ב-NPA
- האימות הבא
- תאימות לבודק עצמאי
מחקר
בינה מלאכותית × הוכחה
08
סיוע בינה מלאכותית ובדיקה עצמאית
ליצור בחופשיות, לאמת בקפדנות
כיוון מחקר שממקם בינה מלאכותית ביצירת מועמדים, בעוד הראיה הסופית נבדקת עצמאית.
- ממצאים
- מחולל מועמדים / תעודה / דוח בודק
- נוכחי
- כיוון מחקר שתואם למודל האמון של NPA
- האימות הבא
- זרימת כתיבה מדודה
לא נמצא תחום מחקר מתאים.
נסו מילת חיפוש אחרת או החזירו את מסנן הבשלות להכול.
Nano Proof Auditor
הפרידו בין יצירת הוכחה לבין הדבר שבו בוטחים.
NPA היא שרשרת כלי הוכחה שמתחילה מתעודות עבור הוכחות תלויות. ממשקי חזית, טקטיקות, חיפוש משפטים, תוספים, בינה מלאכותית, קובצי מקור וסטטוס CI יכולים לעזור ליצור מועמדים, אך אינם ראיית ההוכחה המהימנה.
ניסיוניקוד פתוחAPACHE-2.0
תמונת מצב נוכחית
v0.1.1
מידע ציבורי נבדק ב-2026-06-21.
ליבה עיקרית
Rust
מאמת Rust והליבה הם חלק מצד הבדיקה.
ממצא ביקורת
.npcert
בתי התעודה הקנוניים הם האובייקט לבדיקה.
נקודת בדיקה חוזרת
סקירה ידנית
יש לבדוק את מצב המאגר ואת נראות החבילה לפני פרסום.
חוקר גבולות אמון
עברו בין החלקים כדי לראות במה בוטחים ובמה לא.
לחצו על כל צומת כדי לבדוק מה הוא עושה, מה הוא מפיק ואיזו בדיקה עדיין נדרשת.
לא מהימן
נבדק
גבול חשוב
NPA אינו כרגע תחליף מעשי ל-Lean או Rocq. הדף מסביר תכנון מחקר שממוקד בתעודות ואינו מבטיח מערכות מסחריות ללא באגים או פתרון משפטים אוטומטי.
בדיקת תעודה / סימולציה מסבירה
התנסו בזרימת בדיקת התעודות.
האינטראקציה בדפדפן מסבירה את זרימת הבדיקה. היא אינה מריצה NPA, Rust, WASM או תעודות הוכחה אמיתיות.
דוגמת CLI
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 האם אתם סומכים על הוכחות שנוצרו בידי בינה מלאכותית כפי שהן?
לא. בינה מלאכותית, חיפוש וטקטיקות עוזרים ליצור מועמדים. אנחנו מתמקדים בשאלה האם התעודה הסופית מתקבלת על ידי בודק עצמאי מנתיבי היצירה האלה.
04 האם אימות פורמלי מסיר את כל הבאגים?
לא. שיטות פורמליות בודקות תכונות מסוימות מול מפרט מפורש. מפרטים שגויים, קוד מחוץ לתחום, תפעול ושירותים חיצוניים עדיין דורשים סקירה נפרדת.
05 האם זה קשור לעבודה על מערכות עסקיות?
כן. בדרך כלל מיישמים את המשמעת הזו בהדרגה: אילוצים, נימוקי תוצאה, היסטוריית חישוב, גבולות הרשאה ובדיקות ללוגיקה עסקית חשובה.
דיון בבעיה
אפשר לדון בעבודה שצריך לפתור, לא רק בנושא המחקר.
התחילו מהגיליון הנוכחי, מהכללים ומהמקומות שבהם אנשים מתקנים החלטות. אפשר לברר אם מידול מתמטי, אוטומציה לפי כללים או אבטיפוס צריכים לבוא קודם.
תמונת מצב של מקורות / 2026-06-21
הטענות על NPA מבוססות על תמונת מצב של מאגר finitefield-org/npa. המיקום של Lean ו-Rocq מבוסס על האתרים הרשמיים שלהם. מצב המאגר, התגים האחרונים ונוסח סקירת השיטה נבדקו ב-2026-06-28.