پوانکاره، سطر به سطر وارسی‌شده به دست ماشین
وارسی یک اثبات یکی از طاقت‌فرساترین کارها در ریاضیات است، به‌ویژه وقتی استدلالی چند حوزه را دربرمی‌گیرد. با شتاب گرفتن تولید اثبات‌ها به کمک هوش مصنوعی، وارسی قابل اعتماد اهمیت بیشتری می‌یابد. دستیارهای اثبات (proof assistants) مانند Lean 4 یک پاسخ پیش می‌نهند: تعریف‌ها، گزاره‌ها و اثبات‌ها به صورت کد نوشته می‌شوند و هستهٔ کوچک و مورد اعتماد نرم‌افزار، یعنی «کرنل» آن، هر گام را وارسی می‌کند. اثباتی که از کرنل بگذرد، گزاره‌اش را ثابت کرده است؛ آنچه برای انسان‌ها می‌ماند این است که بررسی کنند گزاره واقعاً همان چیزی را می‌گوید که ریاضی‌دانان در نظر دارند.
اثباتی فشرده، کتابخانه‌ای ناموجود
حدس پوانکاره که پرلمان اثباتش کرد، می‌گوید هر خمینهٔ (manifold) سه‌بعدی بسته و ساده‌همبند — به زبان ساده، فضایی سه‌بعدی و متناهی بدون سوراخی که یک حلقه بتواند در آن گیر کند — هم‌ارز کرهٔ سه‌بعدی است. این اثبات از برنامهٔ شارش ریچی (Ricci flow) پیروی می‌کند که ریچارد همیلتون آغاز کرده بود. سه پیش‌انتشار پرلمان در ۲۰۰۲ تا ۲۰۰۳ استدلال‌های کلیدی را به شکلی بسیار فشرده ارائه کردند؛ پس از آن شرح‌های مفصلی آمدند، از جمله تک‌نگاری ۲۰۰۷ جان مورگان و گانگ تیان که این پروژه از آن پیروی می‌کند.
آن اثبات بر آنالیز هندسی‌ای تکیه دارد که کتابخانهٔ جمعی Lean، یعنی Mathlib، تا حد زیادی فاقد آن بود. بخش بزرگی از پایه‌ها باید از صفر ساخته می‌شد.
نقطه‌عطف‌هایی که ریاضی‌دانان منجمدشان کردند
ژی‌یوان ژانگ، اکسل دولاوال، بین دونگ، چون‌لی لیو و همکارانشان در دانشگاه پکن و دیگر نهادهای پکن، کار را در مه ۲۰۲۶ آغاز کردند: سه «مهندس هوش مصنوعی» با آموزش ریاضی در کنار ریاضی‌دانان. رویکرد نخستشان — صوری‌سازی بخش‌های بزرگی از نظریهٔ پایه — کند بود و کد حاصل از انتظاراتشان پایین‌تر ماند.
در سپتامبر ۲۰۲۶، از نو آغاز کردند. اثبات به حدود ۹۰ نقطه‌عطف (milestone) تقسیم شد که هر یک گزاره‌ای دقیق در Lean همراه با تعریف‌های لازمش بود. ریاضی‌دانان این گزاره‌ها را پیش از یا در حین صوری‌سازی بازبینی کردند و سپس منجمد شدند: عامل‌ها نمی‌توانستند آن‌ها را تغییر دهند و هر اصلاحی باید دوباره از دست ریاضی‌دانان می‌گذشت. چون هیچ‌کس نمی‌توانست همهٔ سطرهایی را که عامل‌ها نوشته بودند بخواند، این نقطه‌عطف‌ها به ایستگاه‌های وارسی‌ای بدل شدند که انسان‌ها در آن‌ها ریاضیات را تأیید می‌کردند.
سپس عامل‌ها به‌طور موازی کار کردند، از راه نشست‌های تعاملی با ابزارهای برنامه‌نویسی — عمدتاً Codex و Claude Code — و از راه سامانه‌ای به نام Archon Horizon که «مأموریت‌های» محدودی را به سرورهای بسیار می‌فرستد. یک بات هر مشارکت را کامپایل و موارد پذیرفته‌شده را ادغام می‌کرد. GPT-6-Astra بیشترِ صوری‌سازی گزاره‌ها و ساخت اثبات‌ها را بر عهده داشت؛ Fable-5.1 برای وارسی‌های مستقل، تشخیص کارهای گیرکرده و بازبینی گزاره‌ها به کار رفت.
۲٫۸ میلیون سطر در حدود دو هفته
پس از ماه‌ها آماده‌سازی، صوری‌سازی اصلی کمی بیش از دو هفته طول کشید. اشتراک‌های هوش مصنوعی و سرورهای اجاره‌ای حدود ۲۵ هزار دلار هزینه داشت. این کار هر دو نسخهٔ توپولوژیک و هموار (smooth) قضیه را اثبات می‌کند، به‌طور کامل کامپایل می‌شود و از یک وارسی مستقل در برابر گزاره‌های هدفی که تنها با Mathlib نوشته شده‌اند سربلند بیرون می‌آید.
حجم آن عظیم است: حدود ۳٫۲ میلیون سطر Lean، که با نگه داشتن تنها آنچه قضیهٔ نهایی به آن وابسته است به ۲٫۸ میلیون کاهش یافت. بنا بر شمارش نویسندگان، نزدیک به نیمی از آن نظریهٔ پایه است. یک نتیجهٔ کلاسیک که مورگان و تیان تنها در یک پانویس به آن اشاره می‌کنند — دربارهٔ ساختارهای هموار روی خمینه‌های سه‌بعدی — به‌تنهایی حدود ۶۵۰ هزار سطر شد.
آنچه انسان‌ها همچنان انجام دادند
نویسندگان موانع را در سه دسته جای می‌دهند: شکاف‌های ریاضی، مشکلات پیاده‌سازی در Lean و مشکلات هماهنگی. انسان‌ها دامنهٔ گزاره‌ها را تعیین کردند (برای نمونه، اینکه کی یک نتیجه به سه بعد محدود شود)، استدلال‌های جاافتاده را تشخیص دادند — مانند گامی دربارهٔ فشردگی موضعی (local compactness) که عامل‌ها نمی‌توانستند پیدایش کنند — و فرض‌های پنهان را شکار کردند. درس اصلی آن‌ها: سازمان‌دهی کار به اندازهٔ توانایی عامل‌ها اهمیت داشت. آن‌ها همین نتیجه را از صوری‌سازی اخیر آخرین قضیهٔ فرما به دست Anthropic نیز می‌گیرند که آن هم پس از آنکه تلاش‌های اولیه رشتهٔ وضعیت پروژه را گم کردند، ناچار به شروع دوباره شد.
وارسی‌شده، اما هنوز نامرتب
نویسندگان کار را تمام‌شده نمی‌دانند. کد پر از تکرار است؛ اثبات‌های عامل‌ها همیشه از مسیر مرجع پیروی نمی‌کنند؛ و تبدیل آن به کتابخانه‌ای قابل استفادهٔ دوباره در آنالیز هندسی کار بعدی است. صوری‌سازی مستقل دیگری از همین حدس به دست گروهی دیگر نیز اعلام شده است. امید آن‌ها: اینکه روزی یک ریاضی‌دان به‌تنهایی بتواند با چنین ابزارهایی پژوهش خودش را وارسی کند.
تعارض منافع. گروه از Claude Code و مدل Fable-5.1، هر دو ساخت Anthropic، در کنار GPT-6-Astra استفاده کرد که از راه اشتراک‌های OpenAI به کار رفت و بیشتر کار را انجام داد. مقاله همچنین پروژهٔ خود را با صوری‌سازی آخرین قضیهٔ فرما به دست Anthropic مقایسه می‌کند. این نوشته را Claude نوشته است.