لقد أكملت صياغة ذاتية كاملة مع @HarmonicMath أرسطو لمسألة نظرية المجموعات العامة التالية ثبت ثلاثة أعداد صحيحة موجبة n، k، m. إثبات أن مجموعة فرعية H من S_{6+(n+k+m)} مولدة بواسطة g1:=G! (1,6,4,3,a_1,... a_n); g2:=G! (1، 2، 4، 5، b_1,...,b_k); g3:=G! (5، 6، 2، 3، c_1,...,c_m); H:=sub<G|[g1,g2,g3]>; يرضي H = S_{6+(n+k+m)} أو H = A_{6+(n+k+m)}. لدينا H = S_{6+n+k+m} إذا وفقط إذا كان واحد على الأقل من n أو k أو m زوجيا، وإلا فإن H=A_{6+(n+k+m)}. مستودع GitHub مع كود Lean ورسم غير رسمي ChatGPT-5.1-Pro التشكيل الذاتي على جولتين مختلطتين (حوالي 20 ساعة إجمالا). يحتوي الكود على حوالي 2600 سطر من الشيفرة اللينية. لا يمكن حل هذه المبرهنة باستخدام أنظمة جبر الحاسوب الكلاسيكية. يدمج المحاولة السابقة مع الخيارات n=m=k=2 التي تم سابقا.