۱۳ میلیون خط کد به زبان Lean؛ این حجم عظیم از داده توسط تیمی از عاملهای (Agents) کلود برای تأیید یکی از گریزپایترین حدسهای ریاضی تاریخ تولید شده است. به نقل از گزارش Anthropic که در ۴ سپتامبر ۲۰۲۶ منتشر شد، این هوش مصنوعی توانست نخستین اثبات سرتاسری و بررسیشده توسط ماشین برای «قضیه آخر فرمات» (FLT) را در ۱۱ روز تکمیل کند؛ مأموریتی که جامعه ریاضی انتظار داشت سالها به طول بینجامد.
برای بیش از ۳۵۰ سال، قضیه آخر فرمات — این ادعا که هیچ عدد صحیح مثبتی برای a، b و c در معادله aⁿ + bⁿ = cⁿ برای n > ۲ وجود ندارد — به یکی از بزرگترین چالشهای ریاضی تبدیل شده بود. پیر فرمات در حدود سال ۱۶۳۷ این ادعا را در حاشیه نسخه شخصی خود از کتاب «ارشمیک» اثر دیوفانتوس نوشت. او در آنجا یادداشتی تحریکآمیز و مشهور را اضافه کرد: «اثباتی واقعاً شگفتانگیز برای این موضوع یافتهام، اما حاشیه این کتاب برای گنجاندن آن بیش از حد تنگ است».
در حالی که سر اندرو وایلز در سال ۱۹۹۵ اثباتی انسانی در ۱۲۹ صفحه ارائه کرد، تبدیل این اثبات به زبانی که کامپیوتر بتواند با قطعیت ۱۰۰٪ آن را تأیید کند (فرمالیزاسیون)، یک تلاش دستی طاقتفرسا بود. مسیر وایلز برای رسیدن به این نتیجه پر از دشواری بود؛ او در ژوئن ۱۹۹۳ اثبات خود را در مجموعهای از سخنرانیهای سه روزه ارائه کرد، اما تنها دو ماه بعد، یکی از بازبینها یک شکاف بحرانی در استدلال او پیدا کرد. وایلز یک سال تمام را صرف اصلاح این خطا کرد؛ ابتدا به تنهایی و سپس با همکاری ریچارد تیلور. او در لحظاتی نزدیک بود پروژه را رها کند، اما سرانجام راه حلی یافت. اثبات نهایی که در می ۱۹۹۵ منتشر شد، بر تکنیکهای مدرنی متکی بود که بسیار فراتر از دانشی بود که فرمات در سال ۱۶۳۷ در اختیار داشت. همین موضوع باعث شد جامعه ریاضی به این نتیجه برسد که احتمالاً «اثبات شگفتانگیز» اصلی فرمات نادرست بوده است.
از سال ۲۰۲۴، تلاشی جمعی به رهبری کوین بازارد در امپریال کالج لندن برای کدگذاری این پیچیدگی در دستیار اثبات Lean آغاز شد. مقیاس این چالش عظیم است؛ برای مثال، تنها طرح اولیه (Blueprint) که جامعه ریاضی برای فاز اول پروژه استفاده کرد، ۸۶ صفحه بود. فرآیند فرمالیزاسیون دشوار است زیرا در حالی که اثباتهای انسانی گامهای بدیهی را حذف میکنند، Lean هر مرحله را، هرچقدر هم پیشپاافتاده به نظر برسد، صریح و دقیق میطلبد. علاوه بر این، اثباتهای انسانی بر قرنها آثار منتشر شده متکیاند، در حالی که یک فرمالیزاسیون باید از بخش بسیار کوچکی از ریاضیات شروع کند که پیشتر به صورت رسمی کدنویسی شده است. این رویکرد یادآور دستاوردهای اخیر در این حوزه است، مانند زمانی که Axiom Math با استفاده از Lean 4 توانست قضیه فاصله اعداد اول ۲۴۶ را تأیید کند و گامی مهم در جهت فرمالیزاسیون نظریه اعداد برداشت.
سازوکار خودکارسازی اثبات
این پیشرفت توسط Tianyi Peng، پژوهشگر آنتروپیک و همکار دانشگاه کلمبیا، هدایت شد. او میخواست بداند آیا کلود میتواند سرعت فرمالیزاسیون را افزایش دهد یا خیر. انگیزه پنگ ریشه در دشواری ذاتی تأیید انسانی داشت؛ او در دوران دانشجویی فرصت چاپ مقالهای در Nature را از دست داد چون تنها میتوانست «۹۹٪ مطمئن» باشد که یک اثبات طولانی درست است، نه ۱۰۰٪ مطمئن.
این هوش مصنوعی قضیه جدیدی را کشف نکرد، بلکه عملیات «خودکارسازی فرمالیزاسیون» (Autoformalization) را انجام داد؛ یعنی ترجمه استدلالهای ریاضی موجود به فرمت قابل تأیید توسط ماشین. به طور مشخص، اثبات کلود از نسخه سادهشده اثبات وایلز پیروی میکند که توسط دارمون، دایموند و تیلور ارائه شده است. این اثر در واقع ادغام تاریخ گستردهای از تفکر ریاضی است و از ایدههای گرهارد فری، ژان-پیر سر، کن ریبت، بری مازور، رابرت لنگلندز، جرولد تانل، یوتاکا تانیاما، گورو شیمورا و آندره ویل بهره میبرد.
برای دستیابی به این هدف، کلود از یک ساختار چندعاملی و پلتفرم تخصصی به نام Prove2Me بهره برد. این پلتفرم که توسط پنگ و همکارانش در دانشگاه کلمبیا طراحی شده بود، چندین حالت شکست بحرانی در هوش مصنوعی را حل کرد:
- مدیریت وضعیت: با استفاده از یک گراف جهتدار بدون دور (DAG) از گزارههای قضایا، از گم شدن مسیر پروژه توسط عاملها در حین رشد پروژه جلوگیری کرد. این کار تخریب حافظه را کاهش داد و اجازه داد چندین عامل به صورت موازی کار کنند.
- بهینهسازی منابع: با جداسازی گزارههای قضیه از اثباتهای آنها در فایلهای مجزا، زمان کامپایل Lean و مصرف منابع را به حداقل رساند، در حالی که پیوندهای بین آنها به صورت مستقل حفظ میشد.
- قابلیت جستوجو: توصیات به زبان طبیعی برای هر قضیه، به عاملها اجازه داد تا کارهای قبلی را به شکل مؤثرتری جستوجو و دوباره استفاده کنند، که منجر به یک مسیر اثبات سادهتر شد.
مقیاس و اجرا
حجم خروجی خیرهکننده است. کلود در این مسیر ۳۰,۳۰۰ قضیه را اثبات کرد و از ۲۹,۵۰۰ مورد از این قضایای میانی در اثبات نهایی استفاده نمود. کد نهایی شامل ۱۳ میلیون خط کد Lean است که بیش از ۵ برابر اندازه Mathlib (کتابخانه اصلی جامعه Lean) است. این در حال حاضر بزرگترین اثبات Lean ساخته شده در جهان به شمار میرود.
این فرآیند حدود ۶ میلیارد توکن (Token) خروجی از یک مدل پژوهشی داخلی (مشابه Claude Fable 5.1) مصرف کرد. دخالت انسانی در حد دستورات استراتژیک سطح بالا بود؛ مثلاً پنگ تنها اشاره میکرد که «بررسی ژاکوبین به عنوان یک طرح اولویت بالایی دارد» یا «قضیه مازور را برای اتمام سریعتر پیش ببرید».
همکاری عاملها بدون نقص نبود. در ابتدا برخی تلاشها شکست خوردند چون عاملها وضعیت پروژه را گم میکردند و دیگر به طور مؤثر با هم همکاری نمیکردند. این تلاشهای ناموفق حدود ۷٪ از خطوط غیر-تکراری (non-boilerplate) در اثبات نهایی را تشکیل میدهند. برای مدیریت چنین چالشهایی، ابزارهایی مانند TheoremDB توسعه یافتهاند تا تلاشهای شکستخورده را به پایگاه دادهای از اثباتهای تأییدشده تبدیل کنند و از تکرار خطاها در پروژههای آتی جلوگیری نمایند.
همانطور که عاملها به خط پایان نزدیک میشدند، لاگهای داخلی آنها لحظه موفقیت را ثبت کردند. بخشهایی از تفکرات کلود شامل این جملات بود: «ریشه FLT در سایت Proved خوانده میشود. لحظهای تاریخی (منهای بررسی مجدد)» و «!!! ریشه FLT با کد 62eb32c0 وضعیت PROVED را نشان میدهد. R = T بسته شد و به ریشه منتقل شد. این هدف کمپین است: FLT سرتاسری در prove2me». سرانجام، در ساعت ۰۲:۰۰:۵۷ UTC در ۱۸ اوت ۲۰۲۶، لاگها ثبت کردند: «🏁🏁🏁 ریشه FLT در prove2me تأیید شد... لحظهای تاریخی برای این کمپین».
اعتبارسنجی و تغییر پارادایم
کوین بازارد پس از بررسی اثبات تأیید کرد که این نتیجه تنها بر اصول پایه ریاضیات متکی است و هیچ فرض اضافهای ندارد. یک سیستم مقایسهگر تأیید کرد که گزاره نهایی کلود با گزاره رسمی FLT در Mathlib مطابقت دارد. این یعنی هوش مصنوعی اکنون میتواند فرمالیزاسیونهای چندلایه و مستحکم در جبر، تحلیل هارمونیک، هندسه و نظریه اعداد را مدیریت کند.
این توانایی فراتر از یک قضیه واحد است. در یک آزمایش کوچکتر، پژوهشگران آنتروپیک با استفاده از سه اکانت Claude Max توانستند کاربردهای «روش دایره هاردی-لیتلوود» را فرمالیزه کنند. عاملها با همکاری کامل در Prove2Me، فرمالیزاسیون «قضیه سه عدد اول وینوگرادوف» را تنها در سه روز به پایان رساندند. این نشان میدهد که فرمالیزاسیون مشارکتی نتایج بزرگ حتی با اشتراکهای تجاری هوش مصنوعی امکانپذیر است.
این دستاورد فرضیه «کند بودن فرمالیزاسیون مدرن» را میشکند. تاریخ ریاضیات پر از چالشهای تأیید است:
- حدس کپلر: اثبات توماس هیلز در سال ۱۹۹۸ چهار سال در بازبینی بود و پانلی متشکل از ۱۲ داور تنها به «۹۹٪ قطعیت» رسیدند، تا اینکه هیلز پروژه Flyspeck را با ۲۰ نفر برای فرمالیزه کردن آن رهبری کرد.
- حدس پوانکاره: اثبات گریگوری پرلمان در سال ۲۰۰۲ تقریباً چهار سال و سه شرح ۳۰۰ صفحهای زمان برد تا توسط جامعه ریاضی پذیرفته شود.
- حدس ضعیف گلدباخ: اثبات هارالد هلگفوت در سال ۲۰۱۳ همچنان در حال بازبینی است.
- شکستهای تاریخی: در سال ۱۹۰۸، جایزهای ۱۰۰,۰۰۰ مارک طلای آلمان (معادل ۱ تا ۲ میلیون دلار امروز) برای اثبات FLT تعیین شد؛ تنها در سال اول ۶۲۱ تلاش نادرست ارسال شد. برخی نتایج نادرست سالها پذیرفته شدند و باعث شدند ریاضیدانان دیگر نظریات خود را بر پایههای غلط بنا کنند.
با خودکارسازی این مسیر، هوش مصنوعی به یک داور خطاناپذیر تبدیل میشود که بار را از دوش ریاضیدانان برمیدارد و راهی دقیق برای بررسی ریاضیات تولید شده توسط LLMها فراهم میکند (که در حال حاضر فرآیندی گران و مستعد خطای انسانی است). کوین بازارد اشاره کرد که این تکنیکها منجر به ابزارهای جدیدی برای «ریشهکن کردن خطاها در مجموعه ریاضیات فعلی و کاهش فشار بر داوران» خواهد شد.
علاوه بر این، نوشتن کد Lean باعث بهبود توانایی کلود در اثبات نتایج جدید شده است. مدل از فرمالیزاسیونهای جزئی برای بررسی مستقل فرضیات خود استفاده میکند، شبیه به روشی که برای اطمینان از مسیر درست، شبیهسازیهای عددی مینویسد.
با افزایش حجم اثباتهای ادعایی توسط ریاضیدانانِ مجهز به هوش مصنوعی، صنعت به سمتی میرود که هر نوشتار انسانی باید همراه با یک اثبات فرمالیزه و بررسیشده توسط ماشین باشد. اگرچه اثبات فرمالیزه نباید جایگزین شرحهای قابل درک انسانی شود، اما ممکن است تنها راه عملی برای جامعه ریاضی باشد تا با مشارکتهای تولید شده توسط هوش مصنوعی همگام شود.
برای حمایت از این انتقال، آنتروپیک و سایر آزمایشگاهها حمایت خود از پژوهشگران ریاضیات محض و فرمالیزاسیون را از طریق اشتراکهای رایگان و تخفیفدار، اعتبارات پژوهشی و گرنتهای اختصاصی برای پروژههای بزرگ علمی (مانند بهبود Mathlib یا فرمالیزه کردن قضایای بزرگ دیگر) گسترش دادهاند.
پژوهشگران اکنون میتوانند کل اثبات و یک راهنمای دقیق را در گیتهاب بررسی کنند تا مسیرهای منطقی خاصی را که کلود برای بستن حلقه میراث فرمات طی کرد، درک کنند.
گام بعدی شما
- اگر پژوهشگر ریاضی هستید، مخزن گیتهاب این پروژه را برای بررسی مسیرهای منطقی کلود تحلیل کنید.
- برای پروژههای پیچیده، از ساختار چندعاملی (Multi-agent) برای خرد کردن مسائل بزرگ به زیر-قضیههای قابل اثبات استفاده کنید.
- ابزارهای دستیار اثبات مانند Lean را به عنوان لایه تأیید نهایی برای خروجیهای مدلهای زبانی به کار ببرید.
اما داستان سختافزاری این تحول حتی شگفتانگیزتر است — به تحلیل ما دربارهی تراشههای Blackwell مراجعه کنید.
گفتگو