Anthropic میگوید هوش مصنوعی کلود آن طولانیترین اثبات ریاضی تاریخ را نوشته و از آن برای اثبات رسمی قضیه آخر فرما استفاده کرده است؛ مشکلی که ۳۵۸ سال ریاضیدانان را سردرگم کرده بود.
کلود این کار را در ۱۱ روز، عمدتاً به صورت مستقل، انجام داد و ۱۳ میلیون خط کد تولید کرد که یک کامپیوتر میتواند آن را خط به خط بررسی کند، به جای اینکه فقط به حرف یک ریاضیدان اعتماد شود.
قضیه آخر فرما میگوید نمیتوانید سه عدد صحیح مثبت را بردارید، هر یک را به توانی بالاتر از ۲ برسانید و مجموع دو عدد اول برابر با سومی باشد. او این ادعا را در سال ۱۶۳۷ در حاشیه یک کتاب ریاضی نوشت و افزود که یک "اثبات واقعاً شگفتانگیز" دارد که حاشیه کتاب برای آن خیلی کوچک است.
سپس او درگذشت. ریاضیدانان ۳۵۸ سال بعد را صرف تلاش برای بازسازی آنچه او فکر میکرد دارد، کردند.
اثبات چیزی و بررسی آن دو کار متفاوت هستند
یک اثبات ریاضی زنجیرهای از گامهای منطقی است و اگر یک حلقه شکسته شود، کل آن فرو میریزد. یافتن آن حلقه شکسته، مدفون در جایی در صدها صفحه استدلال فشرده، میتواند سالها از زندگی سایر ریاضیدانان را به خود اختصاص دهد.
رسمیسازی یک اثبات به معنای ترجمه آن به زبانی است که آنقدر دقیق است که یک کامپیوتر میتواند هر گام را به تنهایی و بدون ورود به ذهنیات، تأیید کند.
ریاضیدانان مدتی است که در نظارت بر این موضوع ضعیف بودهاند. یک جایزه آلمانی در سال ۱۹۰۸ به ارزش تقریبی ۱ تا ۲ میلیون دلار به پول امروز، که برای اولین اثبات معتبر این قضیه ارائه شد، تنها در سال اول ۶۲۱ درخواست اشتباه را به خود جلب کرد.
Checking that a major mathematical proof is correct can take years. Formalization—converting the mathematical reasoning into a form computer proof assistants like Lean can verify—can help.
Last month, Claude completed the first formalized proof of Fermat’s Last Theorem, one of… pic.twitter.com/pdT8zwlV4A
— Anthropic (@AnthropicAI) September 4, 2026
اثبات واقعی تا سال ۱۹۹۵، توسط ریاضیدان بریتانیایی اندرو وایلز، ظاهر نشد و با یک پیچش داستانی همراه بود. وایلز راهحل خود را طی سه سخنرانی در ژوئن ۱۹۹۳ اعلام کرد، اما بعداً یک بازبین اشکالی در آن یافت.
او تقریباً یک سال را صرف رفع آن با کمک یک دانشجوی سابق خود، ریچارد تیلور، کرد، نزدیک بود تسلیم شود و سرانجام یک اثبات تصحیح شده ۱۲۹ صفحهای را در می ۱۹۹۵ منتشر کرد. این اثبات بر ریاضیاتی تکیه داشت که در زمان زندگی فرما وجود نداشت، و این دلیل بزرگی است که ریاضیدانان اکنون شک دارند که "اثبات شگفتانگیز" خود فرما هرگز واقعاً کارساز بوده باشد.
کوین بازارد، ریاضیدان کالج سلطنتی لندن، در سال ۲۰۲۴ پروژهای را آغاز کرد تا دقیقاً همان کاری را انجام دهد که کلود تازه انجام داده است: ترجمه اثبات وایلز به Lean، زبانی که کامپیوترها میتوانند آن را بررسی کنند. این نوع کاری است که به ارتشی از ریاضیدانان داوطلب نیاز دارد—طرح کلی خود پروژه ۸۶ صفحه است و بودجه آن تا سال ۲۰۲۹ تضمین شده است.
کلود کل کار را در ۱۱ روز به پایان رساند.
کلود چگونه واقعاً موفق شد
Anthropic در یک پست عمیقتر توضیح میدهد که تیانیی پنگ، که ابزارهای رسمیسازی هوش مصنوعی را با تیمی در کلمبیا میسازد، تصمیم گرفت ببیند کلود تا کجا میتواند به تنهایی پیش برود. دهها عامل کلود به صورت موازی کار میکردند، تعاریف را مینوشتند، نتایج کوچک را اثبات میکردند و آنها را به نتایج بزرگتر تبدیل میکردند، با تقریباً هیچ ورودی انسانی فراتر از یک اشاره گاه به گاه مانند "این قضیه را در اولویت قرار بده".
ابتدا همه چیز به آرامی پیش نرفت. در ابتدا، عاملها مرتباً از آنچه قبلاً اثبات کرده بودند غافل میشدند و همکاری را متوقف میکردند، و این شروعهای کاذب هنوز حدود ۷ درصد از خطوط در اثبات نهایی را تشکیل میدهند.
آنچه مشکل را حل کرد، ابزاری به نام Prove2Me بود که آن نیز توسط تیم پنگ ساخته شده بود. این ابزار به هر عامل یک لیست کارهای زنده یکسان از اثباتهای کوچکتر که هنوز باید انجام میشدند، میداد تا هیچ کس کار را تکرار نکند یا از مسیر خارج نشود. همچنین فایلها را سازماندهی میکرد تا Lean بتواند همه چیز را سریعتر بررسی کند و یادداشتهای انگلیسی سادهای در مورد هر نتیجه نگه میداشت تا عاملها بتوانند به جای اختراع دوباره، از کار یکدیگر استفاده کنند.
تا زمان اتمام کار، کلود بیش از ۳۰,۰۰۰ قضیه پشتیبان را اثبات کرده بود و میلیاردها توکن را مصرف کرده بود، که بر روی یک مدل تحقیقاتی اجرا میشد که Anthropic میگوید تقریباً قابل مقایسه با Claude Fable 5.1 است، نسخهای که بعدها به صورت عمومی منتشر شد. اثبات نهایی ۱۳ میلیون خط است – بیش از پنج برابر اندازه Mathlib، کتابخانه مشترکی که ریاضیدانان قبلاً برای این نوع کار از آن استفاده میکنند.
یک رمان معمولی ۸۰,۰۰۰ کلمه دارد. اثبات کلود معادل ۱۶۰ رمان استدلال منطقی محض است.
پس آیا این واقعاً مهم است؟
بازارد – که نسخه خودش از این پروژه تا سال ۲۰۲۹ بودجهاش تضمین شده است – اثبات کلود را بازبینی کرد و تأییدش را داد و گفت که این قضیه را "بدون هیچ فرضی جز اصول موضوعه ریاضیات" اثبات میکند.
این با کشف ریاضیات کاملاً جدید توسط کلود یکسان نیست، که Anthropic نیز با تحقیقات رمزنگاری خود در اوایل سال جاری ادعا کرده بود. وایلز سه دهه پیش قضیه فرما را اثبات کرده بود – کلود فقط یک رسید قابل بررسی توسط ماشین برای آن ساخته است. این موضوع مهم است زیرا ریاضیدانان به طور فزایندهای با اثباتهای تأیید نشده، از جمله آنهایی که توسط هوش مصنوعی نوشته شدهاند، سریعتر از آنکه انسانها بتوانند آنها را دستی بررسی کنند، روبرو میشوند.
همچنین، این نوع اثباتها قطعی هستند و مستعد خطاهای انسانی نیستند، که در ریاضیات بسیار مهم است.
این یک مشکل جدید نیست. یک اثبات با کمک کامپیوتر برای حدس کپلر چهار سال طول کشید تا یک هیئت بازبینی تنها به "۹۹٪ اطمینان" متعهد شود، و اثبات گریگوری پرلمن برای حدس پوانکاره نیز تقریباً به همین مدت طول کشید تا کاملاً درک شود.
اگر نمیخواهید حرف Anthropic را در مورد هیچ یک از اینها بپذیرید، مجبور نیستید. اثبات کامل ۱۳ میلیون خطی همین حالا در GitHub موجود است، رایگان برای هر ریاضیدانی که وقت کافی برای بررسی دقیق آن، خط به خط، دارد.
