هنا أقدم نسخة ذاتية كاملة من الصياغة الذاتية لورقة رياضيات حديثة (مرة أخرى!) بارانشوك، ستيفان. "تقليل عدد المعادلات التي تعرف مجموعة فرعية من الفضاء 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