نسخة أولية وصول مفتوح
صياغة رسمية بمساعدة الذكاء الاصطناعي لحدس بوانكاريه
نعرض تحويلاً رسمياً بمساعدة الذكاء الاصطناعي لحدسية بوانكاريه إلى Lean 4. بدأ المشروع بقدر محدود من البنية التحتية الرسمية القابلة لإعادة الاستخدام للتحليل الهندسي الذي يقوم عليه البرهان. ولتنظيم هذا العمل، جمعنا مخطط برهان أعده علماء رياضيات مع عبارات محطات واضحة. وقد مكّنت هذه المحطات من عمل الوكلاء بالتوازي، وأعطت ع …