لقد تجاوزت حدا شخصيا، وأنا مندهش قليلا. هذه هي أول برهان مؤتمت بالكامل من قبل مولدات اللغة الكبيرة وذاتي الصياغة لمبرهنة رياضية جديدة. دعوني أوضح المشكلة: لدينا ثلاث دوائر دوارة كل منها ستة مواقع، جميعها تتقاطع في مجموع ست نقاط. أثبت أن مجموعة الحركات التي تولدها هي المجموعة المتماثلة الكاملة S_{12}. هذه مشكلة لاحظتها في الأصل في لغز جميل في لعبة Machinarium من تطوير Amanita Design. المهمة ليست صعبة للغاية، لكنها على ما يبدو تحتوي على برهين: 1. بحث بالقوة الغاشمة على فئات الاقتران لتمثيل جميع التحويلات (قمت بذلك منذ سنوات عديدة لكن لم أنشره). 2. برهان مولد بنموذج اللغة الكبيرة (في هذه الحالة أنجج قبل حوالي ثلاثة أشهر بواسطة GPT-5-Pro)، أو في الواقع برهان، كلاهما يستخدم بطريقة رائعة نظرية جوردان حول المجموعات الأولية (أو نسخة قريبة من الحدود تكون أكثر مباشرة). ( ما كنت أفتقده حتى الليلة هو أداة لصياغة هذا البرهان بشكل تلقائي. بفضل @HarmonicMath، حصلت على إمكانية الوصول إلى برنامجهم الرائع، أرسطو. باختصار، هذا ما فعلته: أ. تولد البرهان تلقائيا باستخدام نموذج لغوي (وقمت بتشغيله عدة مرات للحصول على نسخة محسنة بكثير). ب. قلص البرهان إلى النص الرياضي الجاري—التعريفات، القضايا، اللممات، النظريات—باستخدام البراهين التي قدمها النموذج اللغوي الكبير. ج. شغل نظام أرسطو طوال الليل (عبر واجهة برمجة التطبيقات). هذا الصباح تلقيت نسخة رسمية بالكامل باللغة Lean (حوالي 700 سطر من الكود). الكود يترجم، لذا لدي الآن شهادة تؤكد أن الإثبات الذي تم إنشاؤه من قبل نموذج اللغة الكبير قد أدى بالفعل إلى حل صحيح. علاوة على ذلك، حصلت على دليل مفاهيمي، أفضل من قوتي الغاشمة. أخطط لدفعه أكثر إلى فئة أوسع من مسائل الجبر. إنه مشروع صغير، لكنه بالنسبة لي شخصيا يمثل علامة فارقة. الآن لدي أدوات يمكن أن تساعدني فعلا في اكتشاف وصياغة ودراسة براهين النظريات الرياضية. هذا ليس أمرا بسيطا. الاسئله: 1. كيف سيتوسع هذا في المستقبل؟ 2. كم من التدريب اللازم للنجاح في مثل هذه المهام؟...