Artificial Mathematical Intelligence: Cognitive, (Meta)mathematical, Physical and Philosophical Foundations

این جلد مبانی نظری یک رشته جدید فراپژوهی بین‌رشته‌ای و درون‌رشته‌ای را مورد بحث قرار می‌دهد که می‌توان آن را به اختصار فراتریاضی شناختی نامید. هدف نهایی دستیابی به یک نمونه جهانی از هوش مصنوعی مصنوعی ملموس (AMI). به عبارت دیگر، AMI به دنبال ساخت یک عامل مصنوعی جهانی (ایده‌آل) است که بتواند مسائل رسمی تعاملی را با یک توصیف ریاضی مفهومی به روشی انسانی حل کند. ابتدا دستورالعمل‌های رسمی از دیدگاه‌های فلسفی، منطقی، فرا ریاضی، شناختی و محاسباتی ارائه می‌کند که از وجود رسمی چنین چارچوب جهانی AMI پشتیبانی می‌کند، و بررسی می‌کند که چه مقدار از ریاضیات فعلی می‌تواند به طور کامل توسط یک برنامه کامپیوتری تعاملی تولید شود و چگونه نزدیک به ساخت ماشینی هستیم که بتواند روشی را شبیه سازی کند که یک ریاضیدان مدرن کار حدس های ریاضی قابل حل را از نقطه نظر مفهومی مدیریت می کند.

این تز مبنی بر اینکه امکان فرامدل کردن شغل فکری یک ریاضیدان شاغل وجود دارد، از نظر اکتشافی توسط نظریه محاسباتی ذهن پشتیبانی می‌شود، که فرض می‌کند که ذهن در واقع یک سیستم محاسباتی، و با توجه به این واقعیت که اثبات های واقعی ریاضی، در اصل، حداقل از نظر تئوری، از نظر الگوریتمی قابل تأیید هستند. مقدمه این جلد اصول چندوجهی فراتریاضی شناختی را ارائه می‌کند و در عین حال مروری بر برخی از برجسته‌ترین نتایج در این راستا ارائه می‌کند، با در نظر گرفتن اینکه تمرکز اصلی بر شواهد به سبک انسانی، و نه صرفاً تأیید رسمی.

قسمت اول کتاب مبانی شناختی جدید برنامه ریاضیات را ارائه می‌کند که با ساختن اصلاحات رسمی مفاهیم و حقایق ریاضی (فرا) سر و کار دارد. دوم موقعیت ها و رسمی سازی یک طبقه بندی جهانی از توانایی های شناختی کلاسیک و جدید را توسعه می دهد، و ابزارهای محاسباتی که امکان محاسبه ترکیب های مفهومی رسمی را فراهم می کند، شرح داده می شوند. به طور خاص، یک توصیف شناختی جدید از تز چرچ-تورینگ ارائه شده است. در بخش آخر، نتایج کلاسیک و جدید در مورد تولید همزمان حجم وسیعی از مفاهیم ریاضی قدیمی و جدید و بخش‌های کلیدی چندین اثبات استاندارد در سیستم‌های قیاسی به سبک هیلبرت نیز نشان داده شده است که به صراحت یک شکاف شناخته شده را پر می‌کند. در مکانیزه کردن ریاضیات در مورد تولید مفهومی مصنوعی.

This volume discusses the theoretical foundations of a new inter- and intra-disciplinary meta-research discipline, which can be succinctly called cognitive metamathematics, with the ultimate goal of achieving a global instance of concrete Artificial Mathematical Intelligence (AMI). In other words, AMI looks for the construction of an (ideal) global artificial agent being able to (co-)solve interactively formal problems with a conceptual mathematical description in a human-style way. It first gives formal guidelines from the philosophical, logical, meta-mathematical, cognitive, and computational points of view supporting the formal existence of such a global AMI framework, examining how much of current mathematics can be completely generated by an interactive computer program and how close we are to constructing a machine that would be able to simulate the way a modern working mathematician handles solvable mathematical conjectures from a conceptual point of view.

The thesis that it is possible to meta-model the intellectual job of a working mathematician is heuristically supported by the computational theory of mind, which posits that the mind is in fact a computational system, and by the meta-fact that genuine mathematical proofs are, in principle, algorithmically verifiable, at least theoretically. The introduction to this volume provides then the grounding multifaceted principles of cognitive metamathematics, and, at the same time gives an overview of some of the most outstanding results in this direction, keeping in mind that the main focus is human-style proofs, and not simply formal verification.

The first part of the book presents the new cognitive foundations of mathematics’ program dealing with the construction of formal refinements of seminal (meta-)mathematical notions and facts. The second develops positions and formalizations of a global taxonomy of classic and new cognitive abilities, and computational tools allowing for calculation of formal conceptual blends are described. In particular, a new cognitive characterization of the Church-Turing Thesis is presented. In the last part, classic and new results concerning the co-generation of a vast amount of old and new mathematical concepts and the key parts of several standard proofs in Hilbert-style deductive systems are shown as well, filling explicitly a well-known gap in the mechanization of mathematics concerning artificial conceptual generation.