Axiom Math، شرکتی نوپا که برای ریاضیات سامانه‌های هوش مصنوعی می‌سازد، می‌گوید یکی از طولانی‌ترین اثبات‌های تاریخ را به کدی تبدیل کرده که رایانه می‌تواند گام‌به‌گام آن را وارسی کند. این شرکت در نوشته‌ای با تاریخ ۲۶ اکتبر و یک مخزن عمومی در GitHub که ۲۷ اکتبر اعلام شد، صورت‌بندی Lean 4 از رده‌بندی گروه‌های ساده متناهی (CFSG)، معروف به «قضیه عظیم»، را عرضه کرد و بخش اصلی کار را به گروه‌هایی از عامل‌های AxiomProver نسبت داد که مهندسان و ریاضی‌دانان هدایتشان می‌کردند.
بر پایه این قضیه، هر گروه ساده متناهی یا دوری از مرتبه اول است، یا متناوب، یا عضو یکی از خانواده‌های نوع لی، یا یکی از ۲۶ گروه پراکنده که بزرگ‌ترینشان Monster است. این گروه‌ها اجزای بنیادی همه گروه‌های متناهی به شمار می‌روند. اثبات انسانی آن در حدود ۱۵ هزار صفحه و بیش از ۵۰۰ مقاله از نزدیک به ۱۰۰ نویسنده پراکنده است؛ در ۱۹۸۳ کامل اعلام شد، اما تا انتشار بررسی ۱۲۲۱ صفحه‌ای حالت موسوم به quasithin در ۲۰۰۴ هنوز به کار نیاز داشت.
به گفته Axiom، پروژه ۲۴ روز طول کشید. کانال هماهنگی در اول اکتبر باز شد و از دل منابع منتشرشده نقشه‌ای از اثبات با ۱۰۸ مرحله و حدود ۳۸۰ وظیفه ساخته شد؛ عامل‌ها کار را برمی‌داشتند، پیش‌نیازهای ناقص را به عامل‌های دیگر می‌سپردند و نتیجه را در مخزنی مشترک قرار می‌دادند. عامل‌های راهبر استدلال‌های دشوار را خرد و گزاره‌ها را بازبینی می‌کردند و بقیه به جست‌وجوی نتایج موجود و نوشتن کد Lean می‌پرداختند. حاصل کار حدود ۴۳٫۱ میلیون خط و بنا بر سایت پروژه، ۲٫۰۵ میلیون اعلان است. Axiom نگفته عامل‌ها بر کدام مدل‌های هوش مصنوعی اجرا می‌شدند.
طبق README، این توسعه هیچ sorry ندارد، برای Lean v4.35.0-rc3 نوشته شده، بر Mathlib و پروژه TauCeti تکیه دارد و صورت قضیه رده‌بندی را از همان پروژه گرفته است، و جز اصول موضوعه استاندارد، به چیزی وابسته نیست و از native_decide هم استفاده نمی‌کند. همچنین حدود ۱٫۲ میلیون خط از پروژه Qiuzhen-CFSG در آن به کار رفته است. ساخت کامل پروژه حتی با تغییرهای منتشرنشده در ابزار Lake نزدیک به یک شبانه‌روز طول کشید. کد با مجوز Apache 2.0 منتشر شده است.
شاید جالب‌ترین بخش، چیزهایی باشد که عامل‌ها در طول کار یافتند. Axiom از ۳۴ انحراف قابل‌توجه نسبت به متون منتشرشده خبر می‌دهد که بیشترشان خطاهای کوچک‌اند، اما میان آن‌ها مثال‌های نقضی برای یک گام بستار در مسیر اثبات جان والتر از Unbalanced Group Theorem در سال ۱۹۸۶ هم دیده می‌شود. شرکت تأکید می‌کند که خود قضیه زیر سؤال نرفته است. AxiomProver برای پر کردن این شکاف نتیجه تازه‌ای درباره حفظ ساختار ثابت کرد که بر نظریه مؤلفه‌های ۲-بیشینه رونالد سولومون در ۱۹۷۶ استوار است و در مقاله‌ای جداگانه شرح داده شده؛ ریاضی‌دانان Axiom بعدها استدلال کوتاه‌تری هم یافتند. ریچارد لاینز و رونالد سولومون، از متخصصان این حوزه، مشاور پروژه بودند و در تنظیم فهرست غلط‌نامه‌ای که هنوز منتشر نشده کمک خواهند کرد.
برای مقایسه، قضیه فیت-تامسون که ۲۵۵ صفحه است و تنها یکی از اجزای رده‌بندی به شمار می‌رود، شش سال کار تیمی به رهبری ژرژ گونتیه را لازم داشت تا در Coq صورت‌بندی شود و این کار در ۲۰۱۲ به پایان رسید. Axiom پروژه تازه را ادامه همین سنت و متکی بر Mathlib معرفی می‌کند، نه جایگزینی برای ریاضی‌دانانی که اثبات اصلی را ساختند.
ناظران مستقل به احتیاط توصیه می‌کنند. Neural Brew در گزارشی به تاریخ ۲۷ اکتبر نوشت که هنوز هیچ بررسی مستقل کاملی منتشر نشده و خودش هم نتوانسته تأیید کند که اثبات دوباره ساخته می‌شود. یوسف فرانکو در Arncof نه بازسازی بیرونی پیدا کرد و نه موضعی از نگهدارندگان Lean یا Mathlib؛ او یادآور شد که رشته پیام Axiom در X از ۵۰ میلیون خط و صدها غلط سخن گفته، در حالی که وبلاگ شرکت ۴۳٫۱ میلیون خط و ۳۴ انحراف را ذکر می‌کند، و بسیاری از واکنش‌های پرشور از افرادی مرتبط با شرکت بوده است. Lean تک‌تک استنتاج‌ها را وارسی می‌کند، اما تأیید اینکه گزاره صوری واقعاً همان رده‌بندی را بیان می‌کند بر عهده انسان‌هاست؛ بازبینی‌ای که خود Axiom از متخصصان نظریه گروه‌ها و جامعه Lean خواسته است.