«قضیهٔ عظیم» ریاضی با کمک ده‌ها ایجنت هوش مصنوعی کامل با کامپیوتر چک شد
هوش مصنوعیClaude Opus 5.5خلاصهٔ کامل‌تر
تیم Axiom Math تو این پست اعلام کرده که اولین اثبات کامل و کامپیوتری برای Classification of Finite Simple Groups (یا CFSG) رو منتشر کرده. گروه‌های ساده متناهی (یعنی «اتم‌های» تقارن که بقیهٔ گروه‌های متناهی از اونا ساخته می‌شن) با این قضیه کامل فهرست می‌شن. اثبات اصلی حدود ۱۵ هزار صفحه تو بیش از ۵۰۰ مقاله از حدود ۱۰۰ ریاضی‌دانه و بهش لقب «قضیهٔ عظیم» دادن.
برای این کار اثبات رو تو Lean بازنویسی کردن؛ Lean یه زبان برنامه‌نویسیه که تعریف‌ها و اثبات‌های ریاضی رو اون‌قدر دقیق می‌نویسه که کامپیوتر بتونه هر قدم رو چک کنه. مهندس‌ها و ریاضی‌دان‌های Axiom تو ۲۴ روز گروه‌هایی از ده‌ها ایجنت هوش مصنوعی رو هدایت کردن و خروجی حدود ۴۳٫۱ میلیون خط کد Lean شد. کار به ۱۰۸ milestone و حدود ۳۸۰ تسک کوچیک‌تر تقسیم شده بود.
طبق توضیح نویسنده‌ها، ایجنت‌ها از طریق GitHub issue تسک برمی‌داشتن و نتیجه رو تو Slack گزارش می‌دادن. یه مشکل تکراری این بود که ایجنت‌ها گاهی یه قضیه رو با فرض‌های اضافهٔ اثبات‌نشده ثابت می‌کردن؛ یعنی کار ظاهراً تموم بود ولی واقعاً نه. برای همین ده‌ها هزار خط کد پاک شد و بخشی از کار از نو برنامه‌ریزی شد.
زمان build هم گلوگاه شده بود، چون ایجنت‌ها سریع‌تر از چیزی که Lean بتونه چک کنه اثبات تولید می‌کردن. مهندس‌ها با کش توزیع‌شده بین ماشین‌ها و چک موازی، و بیرون بردن محاسبه‌های سنگین به شکل گواهی‌های جدا، سرعت تأیید رو چند مرتبه بالا بردن.
فرمال‌سازی ایرادهایی تو مقاله‌های منتشرشده رو هم رو کرد. بیشترشون جزئی بودن، مثل غلط تایپی یا فرض جاافتاده، ولی ۳۴ مورد مهم بود. مثلاً تو جلدهای quasithin از Aschbacher و Smith، ایجنت‌ها با گروه SL₂(5) نشون دادن یه تساوی ادعاشده درست نیست. مهم‌ترین مورد به Unbalanced Group Theorem (یا UGT) مربوط بود: تو اثبات John Walter از ۱۹۸۶ یه ادعای کلیدی مثال نقض داشت.
تیم با مشورت Richard Lyons و Ronald Solomon، از ریاضی‌دان‌های اصلی CFSG، یه مسیر جایگزین ساخت و AxiomProver تو این مسیر قضیهٔ تازه‌ای به اسم «Preservation of simple tops» ثابت کرد. نویسنده‌ها می‌گن ارزش کار اینه که حالا وابستگی‌های این قضیه، که خیلی از شاخه‌های ریاضی و حتی فیزیک ازش استفاده می‌کنن، صریح و قابل بررسیه. لیست errata هم برای جامعهٔ نظریهٔ گروه‌ها منتشر میشه.
نکات کلیدی:
- اثبات اصلی CFSG حدود ۱۵ هزار صفحه تو بیش از ۵۰۰ مقاله از حدود ۱۰۰ ریاضی‌دانه.
- خروجی پروژه حدود ۴۳٫۱ میلیون خط کد Lean بود که تو ۲۴ روز تولید شد.
- حدود ۱٫۲ میلیون خط از کار قبلی Qiuzhen-CFSG و کتابخونهٔ Mathlib استفاده شده.
- ۳۴ انحراف مهم از اثبات‌های منتشرشده پیدا و برطرف شد.
- اثبات UGT از John Walter مثال نقض داشت و با یه مسیر جدید و قضیهٔ تازهٔ «Preservation of simple tops» جایگزین شد.
- تیم اثبات «نسل اول» رو فرمال کرده، چون اثبات نسل دوم هنوز کامل نیست.
