اثبات فرما، این بار کامپیوتر تأییدش کرد
هوش مصنوعیClaude Opus 5خلاصهٔ کامل‌تر
قضیهٔ آخر فرما از ۱۶۳۷ روی کاغذ موند و تازه سال ۱۹۹۵ اندرو وایلز یه اثبات ۱۲۹ صفحه‌ای براش منتشر کرد که وارسی‌ش ماه‌ها کار برد. حالا تو یه پست پژوهشی آنتروپیک اومده که Claude تونسته همون اثبات رو formalize کنه، یعنی جوری بازنویسیش کنه که کامپیوتر خودش قدم‌به‌قدم درستیش رو چک کنه. نتیجه اولین اثبات سرتاسری و ماشین‌چک‌شدهٔ این قضیه‌ست.
ابزار کار Lean بوده؛ یه proof assistant، یعنی برنامه‌ای که منطق هر قدم اثبات رو الگوریتمی وارسی می‌کنه. سختی ماجرا اینه که آدم‌ها تو اثبات‌هاشون کلی قدم بدیهی رو جا می‌ندازن ولی Lean باید همه‌چی رو ببینه. Claude تو ۱۱ روز ۳۰٬۳۰۰ قضیه اثبات کرد که ۲۹٬۵۰۰ تاش به اثبات نهایی رسید، و ۱۳ میلیون خط کد Lean نوشت؛ بیشتر از ۵ برابر حجم Mathlib، کتابخونهٔ اصلی ریاضیات فرمال.
به گفتهٔ نویسنده‌ها تلاش‌های اول شکست خورد، چون ایجنت‌ها حالت پروژه رو گم می‌کردن و هماهنگیشون به هم می‌ریخت؛ همون تلاش‌های ناموفق فقط حدود ۷٪ خط‌های نهایی رو ساختن. چیزی که کار رو راه انداخت Prove2Me بود، یه پلتفرم باز از تیانی پنگ و همکاراش تو کلمبیا: یه گراف از صورت قضیه‌ها نگه می‌داره تا ایجنت‌ها بدونن سراغ چی برن، صورت و اثبات رو تو فایل‌های جدا می‌ذاره تا کامپایل سبک‌تر بشه، و برای هر قضیه یه توضیح به زبان طبیعی داره تا بشه دوباره پیداش کرد.
دخالت انسان کم و در حد راهنمایی‌های کلی بوده و کل کار حدود ۶ میلیارد توکن خروجی مصرف کرده. اثبات نهایی رو خود Lean چک کرده، فقط روی سه اصل موضوعهٔ استاندارد تکیه داره و یه ابزار مقایسه هم تأیید کرده که صورت قضیه دقیقاً همونیه که تو Mathlib نوشته شده. کوین بازارد که اثبات رو مرور کرده می‌گه این یعنی فرمال‌سازی خودکار ادبیات ریاضی مدرن دیگه دور از دسترس نیست و میشه باهاش خطاهای متن‌های موجود رو پیدا کرد و بار داوری مقاله‌ها رو کم کرد.
نکات کلیدی:
- اثبات تو ۱۱ روز و تقریباً خودگردان نوشته شد: ۱۳ میلیون خط Lean و ۲۹٬۵۰۰ قضیهٔ میانی
- حجم کد بیشتر از ۵ برابر Mathlib ـه
- مسیر اثبات، نسخهٔ ساده‌شدهٔ کار وایلز از Darmon، Diamond و Taylor رو دنبال می‌کنه
- تلاش‌های شکست‌خوردهٔ اولیه فقط حدود ۷٪ خط‌های نهایی رو ساختن
- یه آزمایش کوچیک‌تر با سه اشتراک Claude Max هم قضیهٔ سه عدد اول وینوگرادوف رو تو سه روز فرمال کرد
