عن هالمو
Halmos هو منتدى للرياضيات حيث يقوم الخادم بالتحقق من الرياضيات، يبدو وكأنه أي تجميع للروابط حتى تلاحظ أن بعض النشرات تحمل علامة لا يمكن أن تنتجها أي كمية من الكتابة الثقة.
المشكلة مع كل منتدى رياضيات آخر
إن كل هذه المواقع لديها حكم واحد على صحة الفكرة: أشخاص آخرين يجادلون. وهذا يعمل بشكل جيد للغاية، وهذا هو أيضاً السبب في أن البرهان الخاطئ المكتوب بطلاقة يتفوق على البرهان الصحيح المكتوب بشكل سيئ، ولهذا السبب تبدو عبارة "لقد تحققت منه" و"أعتقده" متطابقتين في الصفحة.
Halmos يضيف محكم ثان لا يمكن الاحتجاج معه.
ماذا يفعل الخادم فعلا
ضع كتل مسورة في أي وظيفة أو تعليق وسوف يجري هنا، عند التقديم:
| قطاع | ماذا يحدث | هل يمكن أن يكسب ∎? |
|---|---|---|
lean |
تم التحقق من النوع مقارنة بـ Mathlib. النواة تقبل مصطلح الإثبات أو لا تقبله. | نعم |
sage | SageMath يقوم بتشغيله؛ والناتج الحقيقي يتم تثبيته على الوظيفة. | لا |
gp | يديرها (باري/جي بي) | لا |
z3 | Z3 يبحث عن نموذج: أسرع طريقة ل دحض شيء ما | لا |
python | . | لا |
إن الناتج الذي يظهر تحت القطع هو ما طبعته الأداة حرفيا. ولا يوجد ملخص أبدا: فالملخص هو بالضبط حيث يدخل المختلق.
كيف تحاول ذلك، في حوالي دقيقة
- تعليق طبيعي. معظم الوظائف لا يوجد بها رياضيات على الإطلاق ولا شيء هنا يتطلب أيا منها.
- كتابة الرياضيات في الخط مع
$…$أو كتل عرض بها$$…$$. إنها تظهر كرياضيات حقيقية مطبوعة؛ لا شيء يتم تنفيذه، إنها مجرد علامات. انظر 1 - اسأل الآلة كتلة مسورة وموزعة
sage,gp,z3أوpythonلقد تم تنفيذ هذا البرنامج هنا ويتم إرفاق نتائجه بموقعك حرفيا، وهذا دليل وليس دليلا. انظر 1 - رسم شيئاً مع
plot)الجزء اﻷول(pltوnp(الجـاهز) أو تحديد تسلسلoeis: لصق الأعداد الصحيحة ويعود اسمها، إذا كان معروفا. - أثبت شيئاً ما ألف -
leanالكتلة تم فحصها ضد Mathlib. لصق هذا في أي تعليق: انظر 1
```lean
import Mathlib
theorem two_add_two : 2 + 2 = 4 := by norm_num
```
التسجيل هو اسم مستخدم وكلمة سر: لا بريد إلكتروني، لا خطوة تأكيد. كل ما يفعله المدققون الآن هو على الإنترنت. قائمة الانتظار, و كل حالة حية للتحقق من هو على الصفحة الخاصة بالحالةإذا كان أحدهم ضعيفاً، يُقال لك "لا يمكن السير"، ولا يُقال "رُفض" أبداً.
كتابة على وتيرتك الخاصة
إنشاء بريد إلكتروني وتحويل بين الكتابة والعرض المسبق لرؤية الرياضيات الخاصة بك كما القراء. مشاريعكم؛ حفظ المسودة أيضا يعمل بدون JavaScript. المسودة والاستعراضات لا تنفذ أبدا رمز. نشر عندما تكون مستعداً للمشاركة.
استخدم العناوين لبناء قائمة محتويات المقالة. قائمة إدراج تضيف التعاريف، النظرية، البرهان، الأمثلة، الجداول، والروابط. على سبيل المثال:
:::theorem Squares
For every real $x$, we have $x^2 \geq 0$.
:::
:::proof
Explain your argument here.
:::
يقدم مربع إثبات حجة؛ وتوفر علامة التحقق من التحقق المتواضع المقبول. أضف المصادر وماكرو لاتكس الشخصية تحت المحرر، أو حدد الافتراضات في ملفك الشخصي. اختار موضوعا وعلامات حتى يستطيع القراء المهتمون العثور على مقالك.
تحتوي المقالات المنشورة على رابط تحرير المقالة. وتظل التحريرات المحفوظة سرية حتى تنشر التحديث. وتحافظ المقالة على عنوانها، وتظل عمليات التحقق الآلية القائمة مرتبطة بالنص الذي تم التحقق منه.
واصل القراءة معاً
حفظ النشرات إلى قائمة القراءة الخاصة بك ومتابع المؤلفين أو المواضيع لحساب شخصي بعد الردود على رسائلك وتعليقاتك تظهر في الردود الموجهة إليك.
إنشاء كتاب أو سلسلة إضافة فصول، ترتيب ترتيبها، وجعل المحتويات العامة عندما تكون جاهزة. مجموعة خاصة تخفي قائمة محتوياتها؛ مقالاتها تظل منشورة بشكل فردي.
العلامة
∎ يطلق عليه halmos, بعد بول Halmos, الذي قدم رمز نهاية البرهان انه الشيء الوحيد في هذا الموقع الذي يحمل السلطة, لذا انه متعمد صعوبة الحصول على:
- فقط (لين) يمكنه أن يحددها
Trueهو دليل، وليس دليلا. sorry,native_decide, )أ( حديثةaxiom,unsafeوdebug.skipKernelTCالمرفوضة قبل الملف يعمل، لذا الخداع لا يمكن حتى إنفاق الحوسبة.- ويتم ربط السير إلى النص الذي أنتجته بالضبط. وإذا قمت بتعديل النشر، فإن العلامة تصبح قديمة بدلاً من الانتقال إلى كلمات جديدة.
- إذا كان هناك لاعب يسقط ستحصل على "لم يكن بالإمكان تشغيله", أبدا "مرفوض". حالة التحقق عامة لهذا السبب.
The Commons
والتحقق رخيص؛ والاكتشاف ليس رخيصاً. The Commons إن فريق مايكروسوفت هو مجموعة مشتركة من الحوسبة التي تطحن المشاكل المفتوحة التي صوّت عليها هذا المجلس. أي شخص يمكنه المساهمة فيها، ولا أحد يملك النتيجة، وكل تشغيل يمولها هو عام، بما في ذلك تلك التي لم تصل إلى أي مكان، والتي عادة ما تكون المعلوماتية.
من يديرها؟
Halmos مستقل وصغير إذا كان هناك خطأ هنا أسرع طريقة لإثباته هي كتل الخادم يمكن أن تجري. احصل على الاتصال.