الأوراق الرياضية تحتاج إلى تحقق رسمي. عادة ما يتم ذلك بشكل غير رسمي من قبل الحكم. لكن ماذا لو استطعنا الاعتماد على شيء أكثر قوة مثل الصياغة الذاتية في اللين 4 حيث يتم تقليص دور الحكم إلى التحقق الدقيق لصيغ التعريفات والنظريات؟ كان تجميع الكود المولد تلقائيا سيصبح شهادة إثبات. هذا ما حدث في فترة أطول، كما فعلت مع أرسطو @HarmonicMath. شكرا ل @PietroMonticone @llllvvuu على مساعدتهم في إعداد المخطط. هنا أقدم تطويلا ذاتيا صحيحا بالكامل لورقة لصديقي ستيفان بارانشوك حول تسلسلات التقسيمية في تشيبيشيف. الكود يحتوي على حوالي 5000 سطر من اللين غير البسيط للغاية. يصحح كل التناقضات والثغرات في الورقة الرئيسية (حتى أنه يثبت بعض المقترحات المفوضة). سأنشر سلسلة من هذه التجارب، لإثبات أنه في بعض مجالات الرياضيات، بما في ذلك نظرية الأعداد الأولية، والتوافقيات، والتحليل (كل أنواع الأمور التي يغطيها Mathlib)، لسنا بعيدين عن تحول هائل في توثيق صحة الإثباتات. أعتقد أن هذا العام سيكون مليئا بالفوضى!