الصياغة الذاتية مع أرسطو بواسطة @HarmonicMath والهندسة العكسية باستخدام @OpenAI GPT Codex CLI (في الواقع GPT-5.2 مع xhigh وجميع الميزات التجريبية مفعلة). أثناء عملي على تمرين من جبر بورباكي حول المصفوفات، حصلت على ما يقرب من 900 سطر من شيفرة Lean 4 الموثقة بالكامل، بما في ذلك كل تفاصيل البرهان. ثم مررت به - باستخدام إعداد وكيلي مصمم بشكل مناسب - إلى Codex CLI لعكس هندسة ملف LaTeX المقابل، وإعادة بناء خطوات الإثبات مباشرة من Lean، على طريقة براهين ليزلي لامبورت المنظمة. هذا ليس برنامج لانغلاندز بعد، لكننا بحاجة إلى أتمتة هذا النوع من الرياضيات على المستوى المتوسط. وهذا يحدث الآن. قمت ببساطة ببناء إعداد وكيل مناسب، وقمت بتوصيل كل شيء، وجمع النص من بورباكي (حتى هذا الجزء كان يعمل جيدا مع @grok 4.1 وهو رائع لمعاينة LaTeX مباشرة). سأنهي التوثيق وأنشره على GitHub. تحقق من رسم التبعية - أرسطو تعامل مع كل شيء بنفسه. والدليل تفاعلي بالكامل. نحن نعيش الآن في مستقبل العلم!

في هذا المنشور المجتمعي، أود وضع روابط لبعض الألعاب التفاعلية والتفاعلية الجذابة للغاية (المتاحة مجانا) التي تساعد الناس على استكشاف مفاهيم راقية في كل من البرمجة والرياضيات. إذا كنت تعرف مكانا ممتعا آخر للزيارة، فقط انشر أدناه. استمتع! نحن: مجموعة من ألغاز البرمجة الجذابة التي تساعدك على تعلم كيفية إثبات وتشكيل الرياضيات. لن ترى بنفس الطريقة صلابة 5*7=7*5 بعد الآن. NandGame: تصنع معالجك الخاص من الصفر (حتى NAND مصنوع من دوائر أبسط). إدمان شديد وممتع للغاية! فخ الذباب الكمومي: هنا ستكتسب أخيرا بعض الفهم للحسابات الكمومية. ملونة، لا حدود لها، جذابة وعميقة رياضيا جدا. خدش: تعلم البرمجة بطريقة ممتعة. إقليديا: تعلم كيفية تنفيذ البناء باستخدام المسطرة والبوصلة. كان جزءا من التعليم المدرسي سابقا، لكنه الآن تطبيق. ممتع ومفيد جدا. السطحية: حاول إيجاد تضمين رسم بياني يظهر أنه بالفعل مستوي. يا إلهي: المستكشف النهائي للآلات الخلوية. إذا أردت التعمق أكثر: SageMath: إنه نظام جبر حاسوبي قوي مع بناء جملة بايثون. هو مثالي للدورات وتركيب جملة SageMath أقرب بكثير إلى الخطاب الرياضي العادي. أحب تدريس الدورات مع SageMath. جيوجيبرا: يمكنك إجراء براهين وحسابات وتطبيقات تفاعلية. إنها طريقة ممتعة لتعلم العديد من جوانب الرياضيات غير الخريجين. مشاريع العرض في وولفرام: مجموعة من التطبيقات الرياضية التي يمكن أن تساعدك على فهم مواضيع معقدة جدا. لا تحتاج إلى Mathematica لتشغيلها، لكنك تحتاجها لتصميم تطبيقاتك الخاصة. آليات الإثبات (بقلم هيذر ماكبث): إنه كتاب يحتوي على مستودع تفاعلي على GitHub حيث يمكنك معرفة بنية وصياغة جملة Lean بشكل أكثر شمولا. نظرية مصورة للأعداد (بقلم مارتن ه. وايسمان): هذا كتاب دراسي عن نظرية الأعداد الأساسية مع تطبيقات. وهذه التطبيقات متاحة من الموقع كمجموعة من دفاتر Jupyter المجانية التي تعلمك المفاهيم الأساسية. الجبر الخطي الرسومي: بطريقة مصورة وتفاعلية إلى حد ما لتعلم المفاهيم العميقة في الجبر. HomotopyContinuation.jl: هذه طريقة جميلة للغاية وتفاعلية (مع جوليا) لتعلم بعض الأفكار المعقدة جدا من الهندسة الجبرية (المكونات المتصلة، طريقة الاستمرار التشابعي) وتطبيقات على أنظمة جبرية خاصة جدا تأتي من التطبيقات. يمكنك التعرف على جوليا في الطريق. ماثاميز: إنها تجربة من هيلينا فيريل. هندسة جميلة، تبلاط، أنماط. رائع ببساطة. صعب الشرح: N: طريق النينجا: إذا كنت تعتقد أن الرياضيات صعبة. تعلم الصبر بالطريقة الصعبة. تحذير: شديد الإدمان هايبرروغ: يمكنك تعلم الهندسة الزائدة في بيئة rogue-like.

هنا أقدم نسخة ذاتية كاملة من الصياغة الذاتية لورقة رياضيات حديثة (مرة أخرى!) بارانشوك، ستيفان. "تقليل عدد المعادلات التي تعرف مجموعة فرعية من الفضاء n-على حقل منته." حوليات كلية العلوم في تولوز: الرياضياتي، السلسلة 6، المجلد 33، العدد 1 (2024): 177–182. قضيت بضعة أيام في هذا المشروع. أولا، أجريت أرسطو على @HarmonicMath، والذي خلال حوالي 15 ساعة قام بتشكيل البرهان بشكل ذاتي بالكامل. ثم، بمساعدة كبيرة من @PietroMonticone، تمكنت من إعداد نسخة مخططة من البرهان. هذه نسخة تصبح فيها جميع أجزاء التوثيق في LaTeX تفاعلية ويمكن فحصها ودراستها. يمكننا رؤية التبعيات في البرهان ودراسة علاقاتها. في مرحلة المعالجة اللاحقة، استخدمت أيضا Grok Heavy وCodex CLI مع GPT-5.2 في وضع xhigh لكتابة تحليل سطر بسطر للبرهان الرسمي. هذا مفيد جدا للأشخاص الذين ليسوا مبرمجين محترفين في Lean 4. يمكنك حقا استيعاب جميع خطوات البرهان. أريد أن ألخص انطباعاتي وما تعلمته من هذه التجربة. @vladtenev @Leonard41111588 @HarmonicMath @llllvvuu @littmath @AlexKontorovich @jdlichtman @KenOno691 @CarinaLHong @gdb @hongyuan_mei