نظریه نوع هوموتوپی به‌عنوان زبان بنیادی

شرح دقیق مسئله

این پژوهش به توسعه و کاربرد نظریه نوع هوموتوپی (HoTT) به‌عنوان زبانی بنیادی برای ریاضیات می‌پردازد: اهداف پژوهش 1. صورت‌بندی دقیق اصل یکتایی و پیامدهای آن برای معادل‌بودن ایزومورف‌ها 2. توسعه و کاربرد انواع استقرایی بالاتر برای تعریف ساختارهای توپولوژیک 3. بررسی ارتباط میان HoTT و نظریه رسته‌های (∞,1) 4. ساخت مدل‌های سازگار برای HoTT و تحلیل استقلال اصول موضوعه 5. پیاده‌سازی سیستم‌های اثبات خودکار بر پایه HoTT 6. کشف روابط جدید بین هندسه، توپولوژی، و منطق از طریق لنز HoTT 7. بررسی پدیده‌های ریاضی مانند همبندی، هم‌ارزی هوموتوپی و ناوردایی هوموتوپی از دیدگاه نوع‌شناختی اهمیت و کاربرد این پژوهش دارای اهمیت بنیادی و کاربردی است: 1. ارائه بنیانی متحد برای ریاضیات که هم توصیفی و هم محاسباتی باشد 2. از بین بردن شکاف بین ریاضیات “کاغذ و قلمی” و ریاضیات رسمی‌شده کامپیوتری 3. تقویت ارتباط بین نظریه دسته‌ها، توپولوژی و نظریه نوع 4. توسعه سیستم‌های برنامه‌نویسی وابسته به نوع پیشرفته با کاربرد در نرم‌افزارهای مطمئن 5. امکان اثبات خودکار قضایای پیچیده با کمک اثبات‌یارها 6. رفع برخی تناقضات فلسفی در مبانی ریاضیات 7. کاربرد در علوم کامپیوتر نظری، هندسه محاسباتی و هوش مصنوعی