دربارهٔ هلموس
Halmos یک صفحه برای ریاضیات است که در آن کارساز ریاضی را بررسی می‌کند. شبیه هر جمع‌آوری کننده پیوند است تا زمانی که متوجه شوید که برخی از پستها نشانه‌ای دارند که هیچ مقداری از نوشتن مطمئن نمی‌تواند تولید کند.
مشکل با هر انجمن ریاضی دیگه ای
MathOverflow, math.StackExchange, r/math, the arXiv comment sections. همه آنها دقیقاً یک داور درست بودن دارند: دیگران، بحث کردن. این به خوبی کار می‌کند، و همچنین دلیلی است که یک اثبات اشتباه که به خوبی نوشته شده از یک اثبات درست که بد نوشته شده برتری دارد، و چرا "من آن را چک کردم" و "من باور دارم" در صفحه مشابه به نظر می‌رسند.
Halmos یک داور دوم اضافه می‌کند که نمی‌توان با آن بحث کرد.
کارگزار در واقع چه کارهایی انجام می‌دهد
يه بلوک محصور رو تو هر پست يا نظري بذار و اينجا اجرا ميشه، وقتي ارسال ميشه:
| بلوک | چه اتفاقي ميفته؟ | مي تونه پول در بياره ∎? |
|---|---|---|
lean |
نوع در مقابل Mathlib بررسی شد. هسته عبارت اثبات را قبول می‌کند یا نمی‌کند. | آره |
sage | SageMath آن را اجرا می‌کند؛ خروجی واقعی به پست پیچ خورده است. | نه |
gp | . PARI/GP اداره ميکنه | نه |
z3 | Z3 به دنبال مدلی میگرده: سریعترین راه برای رد کردن يه چيزي | نه |
python | پایتون در Sandbox، خروجی متصل شده. | نه |
خروجی نشان داده شده زیر یک بلوک چیزی است که ابزار چاپ کرد ، حرف به حرف. هیچگاه خلاصه: خلاصه دقیقاً جایی است که یک ساختگی در آن قرار می‌گیرد.
How to try it, in about a minute
- به طور طبيعي نظر بده اکثر پست ها اصلا حسابي ندارن و هيچ چيزي اينجا نياز به حسابي نداره
- نوشتن ریاضی در خط با
$…$, یا یک بلوک نمایش با$$…$$. این به عنوان یک ریاضی متنی واقعی نمایش داده می‌شود؛ هیچ چیزی اجرا نمی‌شود. این فقط یک نشانه‌گذاری است. يه نفر رو ببين - از ماشین بپرس یک بلوک برچسب‌دار
sage,gp,z3یاpythonاينجا اجرا ميشه و خروجي اش به پست شما پيوند داده شده، حرفي به حرفي اين مدرک است نه مدرک يه نفر رو ببين - يه چيزي بکشي با
plotبلوک) matplotlib ، باpltوnpآماده)، یا یک دنباله را باoeis: اعداد صحیح را کپی کنید و با نام برمی‌گردد ، اگر شناخته شده باشد. - يه چيزي رو ثابت کن یک
leanبلوک در برابر Mathlib بررسی نوع می‌شود. این را در هر توضیحی بچسبانید: يه نفر رو ببين
```lean
import Mathlib
theorem two_add_two : 2 + 2 = 4 := by norm_num
```ثبت نام فقط با نام کاربر و رمز عبور است: بدون ایمیل، بدون مرحله تأیید. همه چیزهایی که چکرها الان انجام میدهند در صفو هر حالت زنده چکر در صفحه وضعیت: اگه يکي از اونها بهم خورد بهت ميگن "نمي توني اجرا کني" هيچوقت "نبايد اجرا کني"
با سرعت خودتان بنویسید
شروع پست و بین نوشتن و پیش‌نمایش جابه‌جا شوید تا ریاضی خود را همان‌طور که خوانندگان می‌بینند ببینید. تغییرات به صورت خودکار ذخیره می‌شود طرح تو؛ ذخیرۀ پیش‌نویس بدون جاوااسکریپت نیز کار می‌کند. پیش‌نویسها و پیش‌نمایشها هرگز کد را اجرا نمی‌کنند. هنگامی که آماده اشتراک‌گذاری هستید ، منتشر کنید.
برای ساخت فهرست مطالب مقاله از عنوانها استفاده کنید. گزینگان درج تعریفها ، قضیه ها ، اثبات ها ، مثالها ، جدولها و پیوندها را اضافه می‌کند. برای مثال:
:::theorem Squares
For every real $x$, we have $x^2 \geq 0$.
:::
:::proof
Explain your argument here.
:::یک جعبۀ اثبات یک استدلال را ارائه می‌کند؛ یک چک‌کردن Lean پذیرفته شده نشانۀ تأیید را فراهم می‌کند. منابع و макروس LATEX سفارشی را در زیر ویرایشگر اضافه کنید ، یا پیش‌فرضها را در پروفایل شماموضوع و برچسب را انتخاب کنید تا خوانندگان علاقمند بتوانند پست شما را پیدا کنند.
مقالات منتشر شده پیوند ویرایش مقاله دارند. ویرایشهای ذخیره‌شده تا زمانی که به روزرسانی را منتشر کنید خصوصی باقی می‌مانند. مقاله نشانی خود را حفظ می‌کند ، و چک‌آپ‌های ماشین موجود به متنی که چک‌آپ کردند ، وابسته می‌مانند.
با همديگه ادامه بدين
ذخیرۀ مقالات در فهرست خواندن خصوصی خود ، و دنبال کردن نویسندگان یا موضوعات برای یک دنبالۀ شخصی دنباله پاسخ به پستها و دیدگاههای شما در جوابت رو ميدم.
ایجاد کتاب یا مجموعه برای اتصال مقالات منتشر شده شما. اضافه کردن فصلها ، مرتب کردن ترتیب آنها ، و هنگام آماده شدن محتوا را عمومی کنید. یک مجموعه خصوصی فهرست محتوای خود را مخفی می‌کند ، مقالات آن به صورت جداگانه منتشر می‌شوند.
علامت
∎ بهش ميگن 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 مستقل و کوچک است. اگر چیزی در اینجا اشتباه باشد، سریعترین راه اثبات آن یک بلوک است که سرور می‌تواند اجرا کند. باهاش تماس بگير.