۱۳ میلیون خط اثباتی که کسی نمی‌تونه بخونه
هوش مصنوعیخلاصهٔ کامل‌تر
تو این پست اومده که اول باید یه سوءتفاهم رو صاف کرد: آنتروپیک قضیهٔ آخر فرما رو حل نکرده. اندرو وایلز سال ۱۹۹۴ حلش کرد. چیزی که ۴ سپتامبر اتفاق افتاد اینه که یه ماشین، اثبات اون رو تو Lean (یعنی زبونی که ریاضیات رو جوری می‌نویسه که کامپایلر بتونه خودش درستیش رو چک کنه) نوشت و کرنل Lean قبولش کرد. مخزنش هم عمومیه: anthropics/fermats-last-theorem با لایسنس Apache-2.0.
جالب‌ترین بخش فنی اینه که چک کردن، خودِ بیلده. فایل FinalCheck.lean با #guard_msgs و #print axioms کاری می‌کنه که بیلد فقط وقتی سبز شه که اثبات دقیقاً به سه اصل موضوعهٔ propext و Classical.choice و Quot.sound تکیه کرده باشه. یعنی نمی‌تونی این مخزن رو کامپایل کنی و یه اثبات با sorry یا اصل موضوعهٔ اضافه بگیری. دو لایهٔ دیگه هم هست: comparator نسخهٔ v4.33.0 و nanoda که یه کرنل مستقل Lean نوشته‌شده با Rustه و ۱٬۰۵۲٬۲۳۴ گزاره رو بدون خطا پذیرفت.
مقیاسش هم عجیبه: ۶۰٬۴۷۵ ماژول، ۲۹٬۵۱۱ قضیه و حدود ۱۳ میلیون خط Lean، اون هم تو ۱۱ روز و با حدود ۶ میلیارد توکن خروجی. ده‌ها ایجنت روی پلتفرمی به اسم Prove2Me کار می‌کردن که وابستگی قضیه‌ها رو به شکل یه گراف جهت‌دار بدون دور نگه می‌داره. آنتروپیک می‌گه روش کاملاً خودمختار جواب نداد و همین گراف بود که کارو راه انداخت.
حرف اصلی نویسنده اینه که این بار هیچ‌کس تو این ماجرا صورت‌مسئله رو ننوشته. صورت قضیهٔ فرما همونیه که سال ۱۶۳۷ نوشته شده و سال‌ها قبل هم آدم‌هایی که هیچ نفعی تو این نتیجه نداشتن، تو Mathlib به اسم FermatLastTheorem فرمالش کرده بودن. به گفتهٔ نویسنده چیزی که اینو ممکن کرد مدل نبود، حدود ده سال کار بی‌سروصدا روی Mathlib و پروژهٔ FLT کوین بازارد بود که سؤال رو از قبل نوشته بودن.
در عوض دو تا هزینه پیدا شده. اول اینکه بازبینی مستقل از دست سخت‌افزار معمولی خارج شده: بیلد خود آنتروپیک ۵ ساعت و ۳۲ دقیقه با پیک ۱۵۳ گیگابایت رم طول کشید و comparator حدود ۱۵ ساعت وقت و ۳۰۰ گیگابایت رم می‌خواد. دوم اینکه اسم ۲۹٬۵۱۱ قضیهٔ داخلی رو خود پایپ‌لاین ساخته و معنی‌شون لزوماً همونی نیست که به نظر می‌رسه؛ مخزن خودش می‌گه هر جا اسم و صورت قضیه با هم نخوندن، اون چیزی که واقعاً اثبات شده صورت قضیه‌ست. برای همین نمی‌شه این قضیه‌ها رو جای دیگه‌ای سیته کرد یا روشون چیزی ساخت.
کوین بازارد همون روز نوشت که آنتروپیک ازش جلو زده. مرور انسانی این اثبات عملاً یه ممیزی امنیتی بود، نه ریاضی: بازارد فقط خط‌هایی رو دستی خوند که طبق گفتهٔ خود مدل ریاضیات نبودن، تا مطمئن شه چیزی بیلد رو دستکاری نمی‌کنه. نتیجه اینه که هیچ‌کدوم از این ۱۳ میلیون خط فعلاً نمی‌تونه وارد Mathlib شه؛ صف پول‌ریکوئست‌های Mathlib همین حالا ۳٬۰۷۳ تاست و ظرفیت مرور انسانی گلوگاه اصلیه.
نکات کلیدی:
- اثبات ۴ سپتامبر ۲۰۲۶ منتشر شد؛ مخزن anthropics/fermats-last-theorem با لایسنس Apache-2.0.
- بیلد فقط با سه اصل موضوعهٔ propext، Classical.choice و Quot.sound سبز میشه، وگرنه fail می‌کنه.
- ۱۳ میلیون خط Lean، ۲۹٬۵۱۱ قضیه، ۶۰٬۴۷۵ ماژول، تولیدشده تو ۱۱ روز با حدود ۶ میلیارد توکن.
- کرنل مستقل nanoda ۱٬۰۵۲٬۲۳۴ گزاره رو بدون خطا تأیید کرد.
- بازبینی مستقل حدود ۳۰۰ گیگابایت رم می‌خواد، پس دیگه با لپ‌تاپ شدنی نیست.
- Mathlib خودش ۸۷۰٬۷۶۷ خطه و میلیون‌ها چیز رو اثبات می‌کنه؛ این ۱۳ میلیون خط فقط یه چیز رو.
