Axiom Math، یک شرکت مستقر در سانفرانسیسکو که سیستم‌های هوش مصنوعی برای ریاضیات را می‌سازد، اولین اثبات کامل رایانه‌ای از طبقه‌بندی گروه‌های ساده محدود (CFSG) را منتشر کرده است که به طور گسترده به عنوان طولانی‌ترین اثبات در تاریخ ریاضیات توصیف می‌شود. بر اساس اعلام این شرکت، مهندسان و ریاضیدانان گروهی از ده‌ها عامل هوش مصنوعی را طی تنها 24 روز هدایت کردند تا تقریباً 43.1 میلیون خط کد را در دستیار اثبات ناب تولید کنند، و نتیجه‌ای را تأیید کردند که قبلاً تقریباً 15000 صفحه در بیش از 500 ژورنال و 100 مقاله در حدود 100 مقاله نوشته شده بود.

این دستاورد در لحظه ای به دست می آید که ریاضیات به کمک ماشین به سرعت در حال افزایش است و رسانه های ردیابی [اخبار تحقیقات هوش مصنوعی] (https://aibuzzwire.news/en) شاهد حرکت تأیید رسمی از یک تمرین تخصصی به یک قابلیت مرزی هستند. چیزی که این انتشار را غیرعادی می کند مقیاس است: رسمی سازی تقریباً شامل 2.05 میلیون اعلان سازماندهی شده در 100 نقطه عطف است که هر یک از آنها توسط هسته Lean بررسی می شود، هسته کوچک قابل اعتمادی که هر مرحله منطقی را تأیید می کند.

آنچه طبقه بندی در واقع می گوید

گروه‌های ساده محدود بلوک‌های سازنده تقارن محدود هستند و طبقه‌بندی - با نام مستعار «قضیه عظیم» - فهرست کاملی از آنها را ارائه می‌کند. طبق مستندات پروژه، هر گروه ساده محدود یکی از چهار نوع است: یک گروه چرخه‌ای از مرتبه اول، یک گروه متناوب روی حداقل پنج نماد، یکی از شانزده خانواده نامتناهی از گروه‌های نوع Lie که بر روی میدان‌های محدود ساخته شده‌اند، یا یکی از دقیقاً ۲۶ گروه پراکنده که در هیچ خانواده‌ای قرار نمی‌گیرند.

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

ازدحام ماموران در 500 منبع

اثبات اصلی در بیش از 500 مقاله و کتاب پراکنده است که بسیاری از آنها دهه‌ها پیش با نمادهای ناسازگار نوشته شده‌اند. یکی از مهندسان Axiom این روش را در بحث انتشار اخبار هکر توضیح داد: گروهی از ماموران وظیفه یافتن همه این منابع را داشتند که بخش سخت آن مونتاژ همه چیز در یک کل منسجم بود، زیرا همان مفهوم غیررسمی را می‌توان به روش‌های کمی متفاوت اما از نظر ریاضی ناسازگار رسمیت داد.

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

34 انحراف از رکورد منتشر شده

ترجمه اثبات منتشر شده به شکل قابل بررسی ماشینی، مشکلات واقعی را در ادبیات ریاضی آشکار کرد. Axiom گزارش می دهد که اکثر مسائل جزئی بودند - اشتباهات تایپی، اشتباهات در جداول، یا فرضیه های حذف شده. اما 34 انحراف قابل توجه از رکورد منتشر شده وجود داشت که قبل از رسمی شدن باید برطرف می شد.

اساسی ترین به قضیه گروه نامتعادل مربوط می شود. در حالی که یک مسیر نسل اول به نتیجه را رسمی می‌کردند، تیم نمونه‌های متقابلی را برای ادعای پایانی که در یک استدلال منتشر شده استفاده می‌شد، پیدا کرد. با مشورت نظریه پردازان گروه خبره، آنها مسیر جایگزینی را ساختند که بر اساس تکنیک های ساختاری دوران دانیل گورنشتاین - به ویژه نظریه حداکثر 2 مؤلفه از دهه 1970 ساخته شده بود - و اصلاح را به عنوان یک مقاله تئوری گروهی جدید 35 صفحه ای منتشر کردند که به عنوان پیش چاپ 2610.00575 ارسال شد. این شرکت می‌گوید که فهرست طولانی اشتباهی را به نفع جامعه ریاضی منتشر می‌کند که با مشورت نظریه‌پردازان گروهی که طبقه‌بندی بر روی کارشان است، تهیه شده است.

چرا ریاضیات ماشینی بررسی شده مهم است

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

پژواک های عملی در جاهای دیگر در فیزیک نیز وجود دارد. بزرگترین گروه از 26 گروه پراکنده، گروه هیولا، در برنامه "مهتاب هیولایی" ظاهر می شود که تقارن محدود را به توابع مدولار متصل می کند - کاری که ریچارد بورچردز را در سال 1998 مدال فیلدز را به ارمغان آورد - و در پیشنهاد ادوارد ویتن در سال 2007 که سه تقارن هیولا را به همگانی همسانی سیاه و سفید مرتبط می کند. یک طبقه بندی تایید شده، ریاضیات ساختاری زیربنایی را دقیقاً برای این نوع کاربردهای بین رشته ای روی زمین محکم تری قرار می دهد.

بعد چه می آید

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

از هوش مصنوعی جلوتر بمانید

اخبار هوش مصنوعی را بیشتر بخوانید →