Halmos ∎

אודות Hallmos

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

הבעיה עם כל פורום מתמטיקה אחר

MathOverflow, math.StackExchange, r/math, the ArXiv response sections. לכולם יש בדיוק אחד הפוסק של תקינות: אנשים אחרים, מתווכחים. זה עובד בצורה יוצאת דופן, וזו גם הסיבה לכך שהוכחה שגויה שנכתבה באופן שוטף עולה על זכות אחת כתובה בצורה גרועה, ומדוע "בדקתי את זה" ו"אני מאמין שזה נראה זהה על הדף.

Halmos מוסיף פוסק שני שלא ניתן להתווכח איתו.

מה שהשרת עושה באמת

שים בלוק מגודר בכל הודעה או הערה וזה פועל כאן, על כניעה:

בלוקמה קורה?האם זה יכול להרוויח ∎?
lean הסוג נבדק נגד Mathlib. הגרעין מקבל את המונח הוכחה או שזה לא. כן.
sageסייג'מת' מפעילה את זה, הפלט האמיתי מוצמד לעמדה.לא.
gpפרי / GP מנהל אותו.לא.
z3Z3 מחפש מודל: הדרך המהירה ביותר הפריך משהו.לא.
pythonתיבת חול פייטון, פלט מצורף.לא.

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

איך לנסות את זה, בעוד דקה בערך.

  1. תגובה רגילה. לרוב העמדות אין בכלל מתמטיקה ושום דבר כאן לא דורש שום תשובה.
  2. כתוב קו מתמטי עם $…$או בלוק תצוגה עם $$…$$. זה הופך לחישובי סוג אמיתיים; שום דבר לא יוצא להורג. לראות אחד
  3. שאל את המכונה. בלוק מגודר מתויג sage, gp, z3 או python הוא יוצא להורג כאן, והפלט שלו מחובר לעמדה שלך, מילה במילה. לראות אחד
  4. צייר משהו עם plot בלוק (עם פלטליב, עם plt ו np מוכן), או לזהות רצף עם oeis: הדבק את המספרים השלם והוא חוזר בשם, אם הוא ידוע.
  5. תוכיח משהו. א. lean בלוק נבדק סוג נגד Mathlib. הדבק את זה לכל הערה: לראות אחד
```lean
import Mathlib
theorem two_add_two : 2 + 2 = 4 := by norm_num
```

ההרשמה היא שם משתמש וסיסמה: אין דוא"ל, אין שלב אישור. כל מה שהדמקה עושה כרגע נמצא על גבי ה-Deckers. תור, and each checker's live state is on the עמוד מצבאם אחד מהם נפל, נאמר לך "לא יכול לברוח," מעולם לא "נדחה."

כתוב בקצב שלך

התחל עמוד ולהחליף בין כתיבה לתצוגה מקדימה כדי לראות את המתמטיקה שלך כמו שקוראים יעשו. שינויים נשמרים אוטומטית הטיוטות שלך; Save draft also works without JavaScript. Drafts and previews never run code. Publish when you are ready to share.

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

:::theorem Squares
For every real $x$, we have $x^2 \geq 0$.
:::

:::proof
Explain your argument here.
:::

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

לפרסומים שפורסמו יש קישור ל- Edit. העריכה נשמרת נשארת פרטית עד שאתה מפרסם את העדכון. המאמר שומר את כתובתו, ובדיקות מכונה קיימות נשארות קשורות לטקסט שהם בדקו.

המשיכו לקרוא יחד

שמור הודעות לרשימת הקריאה הפרטית שלך ועקוב אחר סופרים או נושאים אישיים הבא feed. Replies to your posts and comments appear in עונה לך.

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

הסימן

∎ נקרא halmos, after Paul Halmos, who introduced the end-of-proof symbol. It is the only thing on this site that carries authority, so it is deliberately hard to get:

  • רק ליאן יכול לכוון את זה. True זו ראיה, לא הוכחה.
  • sorry, native_decide, טרי axiom, unsafe ו debug.skipKernelTC נדחה לפני הקובץ פועל, כך רמאי לא יכול אפילו לבזבז מחשב.
  • ריצה מחוברת לטקסט המדויק שיצר אותה. ערוך את הפוסט והסימן הולך מעופש ולא העברה למילים חדשות.
  • אם בודק הוא למטה אתה מקבל "לא יכול לרוץ"לעולם לא. "נדחה". מצב בודק הוא ציבורי מסיבה זו.

בני הבית

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

מי מנהל אותו?

Halmos הוא עצמאי וקטן. אם משהו כאן לא בסדר, הדרך המהירה ביותר להוכיח את זה היא בלוק השרת יכול לרוץ. צור קשר.

הצטרף לשיחה.

להירשם לכתוב, לחסוך רעיונות, ולעקוב אחרי האנשים שעוררו בך השראה.

צור חשבון · שכחת את הסיסמה?

שם משתמש וסיסמא הם כל מה שאתה צריך כדי להתחיל.

שלח לנו משוב

ספר לנו מה קרה או למה ציפית, קראנו כל הודעה.

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