ציין את הטענה, הליבה תחליט אם היא הוכחה.

לוח מודלים תוקף את הבעיה שלך עם הספרות, SageMath, PARI/GP ו-SMT פותר, ואז פורמלית התוצאה ב-Lean 4 נגד Mathlib. הגרעין של ליאן מקבל את ההוכחה או לא, ושום כמות של פרוזה בטוחה משנה זאת. כאשר היא נכשלת, אתה מקבל את המטרה המדויקת שנותרה,

המטרה

תהיה ספציפי לגבי מה שבוצע אומר. "תבחין אם X הוא נכון, ותוכיח את זה" פעימות "ספר לי על X"

הבר חייב להיות פנוי.

Careful expert

What a competent professional in the field would accept as done and correct.

Publication standard

Would survive peer review: every claim sourced or derived, methods stated, limitations acknowle…

Formal proof

A complete deductive argument. Every step justified, every assumption stated, no appeals to pla…

Prize standard

The bar a Clay Millennium Prize submission would face: a complete, self-contained, gap-free pro…

Decision-grade

Enough evidence to act on commercially: options costed, risks named, recommendation justified.

Write my own

Describe your own standard.

השופט מחזיק בבר הזה פשוטו כמשמעו, בקש הוכחה ברמה גבוהה, והיא תגיד לך בפשטות מתי הפאנל יתמוטט,

הלוח

יותר מושבים פירושם יותר זוויות, ויותר עלויות לסיבוב.

שופט

חוקים על הקריטריונים ובודק מחדש כל ראיה שווה את המודל החזק ביותר שלך

סיבובים

& גבול הוצאות

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

ראות

הוצאה לאור בסיום

הרשם כדי להתחיל משחק

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

דמקה שאי אפשר לשכנע אותה

Lean 4 with Mathlib type-checks the final statement, and a proof that leans on sorry, native_decide or a fresh axiom is rejected rather than counted. Alongside it: SageMath, PARI/GP, Z3, CVC5 and the OEIS, so a construction can be computed and identified before anyone tries to prove anything about it.

הוכחה כושלת היא ממצא.

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

שום דבר לא הוכח פעמיים.

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