בערך Theorem.chat
Theorem.chat לוקח טענה מתמטית ומנסה ליישב אותה. אתה קובע את הטענה, ואת הסטנדרט שיש לה לפגוש. פאנל של מודלים AI □ כמה שאתה רוצה, מכל ספק שאתה רוצה לתקוף אותה, ועוד דגם של שופטים. אז הטיעון הוא רשמי ב- Lean 4 נגד Mathlib, והגרעין Lean מחליט אם זה הוכח. השלב האחרון הוא המוצר.
למה גרעין, ולא מודל אחר
שאל מודל שאלה קשה ואתה מקבל תשובה שוטפת האם זה נכון או לא. שאל כמה מהם והם מסכימים לעתים קרובות, אשר מרגישים כמו אימות והוא לא: מודלים חולקים נתונים אימונים ולחלוק כתמים עיוורים. מודל שני בדיקה ראשונה היא עדיין אותו סוג של שיפוט, וזה יכול להיות דיבר עגול. הליבה הנטויה לא יכולה. זה גם נובע מההצהרה מן האקסיומס ו-Mathlib, או זה לא, ולא בטוח אין השפעה על התוצאה.
הדרכים הרגילות לזייף הוכחה רשמית נבדקות וסירבו. הוכחה שמשאירה חור עם sorry, אחת שפונה ל-native_decide כדי לגרום לגרעין לקחת חישוב על אמון,
מה הפאנל באמת יכול לעשות
הלוח עובד עם הספרות arXiv, Open Alex, Crossref ▪ Crossref ▪ אז תוצאה ידועה היא במקום re-dived בצורה גרועה. יש לו SageMath ו-PARI/GP עבור חישוב, Z3 ו-CVC5 עבור SMT פתרון, OEIS חיפוש מחדש עבור זיהוי רצף זה בנה, וסביבת פייטון עם גישה לרשת. השערה יכולה להיבחן נגד עשרת אלפים מקרים לפני שמוציאים את הדיון, כדי להוכיח את העימות על מנת לבטל את העימות.
ראיות, לא צנות.
match אינו מבקיע על איכות הויכוח. הטענה היא רק לפרק לקריטריונים קבלה, וקריטריון מיושב רק כאשר משהו מאחורי זה יכול להיבדק שוב על ידי צד שלישי: מקור עם המעבר הרלוונטי מצוטט, או קוד אשר הוצא להורג עם התפוקה האמיתית שלו. השופט בודק שוב את הראיות לפני פסיקה, והוא לא יכול להכריז על match גמור בזמן שקריטריון עדיין פתוח.
אתה קובע את הרף.
אתה יכול לבחור את הסטנדרט, והשופט מחזיק בו פשוטו כמשמעו. בקש מה מומחה זהיר יקבל ואתה מקבל את זה. בקש טיעון דדוקטיבי מלא עם כל הנחה מוצעת
כדי להיות ברור לגבי זה: זו לא מכונה שנותנת לבעיות פתוחות. זו מכונה שמסרבת לאפשר לויכוח לעבור כמוסכם כאשר הוא לא, וזה אומר לך בדיוק איזה צעד נכשל.
פורמליזציה כושלת היא התפוקה המועילה
כאשר ליאן לא תסגור את ההוכחה, תקבלו את המטרה המדויקת שנותרה. בפועל, זה כמעט תמיד המקום שבו הטיעון הלא רשמי היה
עבודה ארוכה שורדת
כל Lemma הבסיסים קובעים הולך לתוך ספר חשבונות משותף עם ההוכחה שלה, כך תוצאות נכתבות פעם אחת ומעולם מחדש, ומבוי סתום נרשם כך שאף אחד לא הולך בחזרה אליהם. Matches לרוץ לצד השרת ולעצור באופן נקי ▪ על תקציב, על הפסקות ספק, או בגלל שאתה סגור את הכרטיסייה
מה זה לא עבור
Theorem is a deductive word. This site is built for mathematics, logic, theoretical computer science, theoretical physics and economic theory — fields where a claim is settled by proof. Empirical questions in biology, medicine, chemistry or the social sciences do not produce theorems, they produce findings, and no amount of formalisation will decide them. Our sister site referee.chat runs the same panel-and-referee process without the Lean step, for exactly those questions.