אודות Hallmos
Halmos הוא לוח למתמטיקה שבו השרת בודק את המתמטיקה. זה נראה כמו כל אגרגטור קישור עד שאתה שם לב שכמה פוסטים נושאים סימן לא כמות בטוחה של כתיבה יכולה לייצר.
הבעיה עם כל פורום מתמטיקה אחר
MathOverflow, math.StackExchange, r/math, the ArXiv response sections. לכולם יש בדיוק אחד הפוסק של תקינות: אנשים אחרים, מתווכחים. זה עובד בצורה יוצאת דופן, וזו גם הסיבה לכך שהוכחה שגויה שנכתבה באופן שוטף עולה על זכות אחת כתובה בצורה גרועה, ומדוע "בדקתי את זה" ו"אני מאמין שזה נראה זהה על הדף.
Halmos מוסיף פוסק שני שלא ניתן להתווכח איתו.
מה שהשרת עושה באמת
שים בלוק מגודר בכל הודעה או הערה וזה פועל כאן, על כניעה:
| בלוק | מה קורה? | האם זה יכול להרוויח ∎? |
|---|---|---|
lean |
הסוג נבדק נגד Mathlib. הגרעין מקבל את המונח הוכחה או שזה לא. | כן. |
sage | סייג'מת' מפעילה את זה, הפלט האמיתי מוצמד לעמדה. | לא. |
gp | פרי / GP מנהל אותו. | לא. |
z3 | Z3 מחפש מודל: הדרך המהירה ביותר הפריך משהו. | לא. |
python | תיבת חול פייטון, פלט מצורף. | לא. |
הפלט המוצג מתחת לבלוק הוא מה שהמודפס, מילה במילה. אף פעם לא סיכום: סיכומים הם בדיוק היכן שזיוף יחליק פנימה.
איך לנסות את זה, בעוד דקה בערך.
- תגובה רגילה. לרוב העמדות אין בכלל מתמטיקה ושום דבר כאן לא דורש שום תשובה.
- כתוב קו מתמטי עם
$…$או בלוק תצוגה עם$$…$$. זה הופך לחישובי סוג אמיתיים; שום דבר לא יוצא להורג. לראות אחד - שאל את המכונה. בלוק מגודר מתויג
sage,gp,z3אוpythonהוא יוצא להורג כאן, והפלט שלו מחובר לעמדה שלך, מילה במילה. לראות אחד - צייר משהו עם
plotבלוק (עם פלטליב, עםpltוnpמוכן), או לזהות רצף עםoeis: הדבק את המספרים השלם והוא חוזר בשם, אם הוא ידוע. - תוכיח משהו. א.
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 הוא עצמאי וקטן. אם משהו כאן לא בסדר, הדרך המהירה ביותר להוכיח את זה היא בלוק השרת יכול לרוץ. צור קשר.