🧮 صوری‌سازی قضیه آخر فرما توسط عامل‌های Claude
در یک دستاورد بی‌سابقه، عامل‌های هوش مصنوعی Claude به‌طور خودکار و در مدت ۱۱ روز، اثبات کامل قضیه آخر فرما (Fermat's Last Theorem) را در زبان برنامه‌نویسی Lean صوری‌سازی کردند. این اولین بار است که یک اثبات ریاضی در این سطح از پیچیدگی، به‌طور کامل توسط یک سیستم غیرانسانی و قابل‌بررسی توسط کامپیوتر تولید می‌شود.
---
📜 اهمیت قضیه آخر فرما
این قضیه که در سال ۱۶۳۷ توسط پییر دو فرما مطرح شد، می‌گوید معادله‌ی aⁿ + bⁿ = cⁿ برای هیچ عدد صحیح مثبتی با توان بیشتر از ۲ جواب ندارد. اثبات آن ۳۵۰ سال و تلاش نسل‌ها ریاضیدان را به خود اختصاص داد و نهایتاً در سال ۱۹۹۵ توسط سر اندرو وایلز با ۱۲۹ صفحه و پس از ۷ سال کار فشرده به پایان رسید. صوری‌سازی این اثبات، یعنی تبدیل آن به زبانی که کامپیوتر بتواند گام‌به‌گام بررسی کند، سال‌ها هدف جامعه‌ی ریاضیات بوده است.
---
🤖 روش انجام و ارقام کلیدی
این پروژه با همکاری ده‌ها عامل Claude (با استفاده از مدلی قابل‌مقایسه با Claude Fable 5.1) و با بهره‌گیری از پلتفرم Prove2Me (که توسط تیان‌یی پنگ از دانشگاه کلمبیا توسعه یافته) انجام شد. فرآیند به این شکل بود:
· زمان انجام: ۱۱ روز
· تعداد خطوط کد Lean تولیدشده: ۱۳ میلیون خط
· تعداد قضایای میانی اثبات‌شده: ۳۰,۳۰۰ قضیه (که ۲۹,۵۰۰ تای آنها در اثبات نهایی استفاده شدند)
· هزینه‌ی توکن: حدود ۶ میلیارد توکن خروجی
· تعداد عامل‌های همکار: ده‌ها عامل که به‌صورت موازی و با حفظ وضعیت پروژه کار می‌کردند
پلتفرم Prove2Me با نگهداری یک گراف جهت‌دار از قضایا، به عامل‌ها امکان می‌داد تا به‌صورت موازی و بدون تداخل، بر روی بخش‌های مختلف اثبات کار کنند و از گم‌شدن وضعیت پروژه جلوگیری کند.
---
✅ تأیید صحت و اهمیت آن
اثبات تولیدشده توسط کامپایلر Lean و یک Comparator رسمی بررسی شده و صحت آن تأیید شده است. کوین بازارد، ریاضیدان برجسته‌ی مسئول پروژه‌ی صوری‌سازی این قضیه از سال ۲۰۲۴، این دستاورد را «فوق‌العاده» خوانده و تأیید کرده است که اثبات، تنها بر اساس سه اصل موضوعه‌ی استاندارد لین استوار است.
---
💡 چشم‌انداز آینده
· کاهش بار بررسی‌های انسانی: با افزایش اثبات‌های تولیدشده توسط هوش مصنوعی، صوری‌سازی خودکار می‌تواند فرآیند تأیید را که گاه سال‌ها طول می‌کشد، به شدت کاهش دهد.
· اعتماد به ریاضیات: این روش می‌تواند به کشف خطاهای بالقوه در انبوه عظیم ادبیات ریاضی کمک کند.
· دسترسی همگانی: در یک آزمایش کوچک با سه حساب کاربری شخصی Claude Max، عامل‌ها موفق شدند در تنها ۳ روز قضیه‌ی سه‌پرایم وینوگرادوف را صوری‌سازی کنند که نشان می‌دهد این قابلیت به‌زودی در دسترس عموم قرار خواهد گرفت.
محققان آنتروپیک معتقدند که به‌زودی تولید یک اثبات رسمی در کنار هر مقاله‌ی ریاضی، به یک رویه‌ی رایج تبدیل خواهد شد.
👩🏫 تعریف:
فرمالیزاسیون (یا صوری‌سازی) در ریاضیات، به فرآیند تبدیل تعاریف، قضایا و برهان‌های ریاضی از زبان معمولی انسان به یک زبان دقیق، سخت‌گیرانه و قابل‌فهم برای کامپیوتر گفته می‌شود تا هرگونه ابهام کاملاً از بین برود.
صوری‌سازی چگونه کار می‌کند؟
حذف شهود فردی: بیان غیر رسمی ریاضی به زبان طبیعی (مانند فارسی یا انگلیسی) اتکا دارد که در آن گاهی مراحل اثبات با جملاتی مثل «واضح است که...» نادیده گرفته می‌شوند. صوری‌سازی تمام گام‌های منطقی را به اصول موضوعه پایه و قوانین استنتاج صریح تجزیه می‌کند.
دستیارهای اثبات: ریاضیدانان برای نوشتن و تأیید خودکار این برهان‌ها از نرم‌افزارهایی به نام «دستیار اثبات» (یا اثبات‌کننده تعاملی قضایا) مانند Lean، Coq، Agda و Isabelle/HOL استفاده می‌کنند.
نحو (Syntax) سخت‌گیرانه: هر عبارت باید از قوانین ساختاری و برنامه‌نویسی دقیقی پیروی کند تا کامپیوتر بتواند با اطمینان ۱۰۰ درصد تضمین کند که هیچ خطای منطقی در اثبات وجود ندارد.
---
🔗 مطالعه‌ی کامل و دسترسی به اثبات:
anthropic.com/research/formalizing-fermats-last-theorem
💻 مخزن گیت‌هاب اثبات:
github.com/anthropics/fermats-last-theorem
---
#Anthropic #ریاضیات_رسمی #قضیه_آخر_فرما #هوش_مصنوعی #پیشرفت_علمی #Lean
🆔 @asrgooyeshpardaz
در یک دستاورد بی‌سابقه، عامل‌های هوش مصنوعی Claude به‌طور خودکار و در مدت ۱۱ روز، اثبات کامل قضیه آخر فرما (Fermat's Last Theorem) را در زبان برنامه‌نویسی Lean صوری‌سازی کردند. این اولین بار است که یک اثبات ریاضی در این سطح از پیچیدگی، به‌طور کامل توسط یک سیستم غیرانسانی و قابل‌بررسی توسط کامپیوتر تولید می‌شود.
---
📜 اهمیت قضیه آخر فرما
این قضیه که در سال ۱۶۳۷ توسط پییر دو فرما مطرح شد، می‌گوید معادله‌ی aⁿ + bⁿ = cⁿ برای هیچ عدد صحیح مثبتی با توان بیشتر از ۲ جواب ندارد. اثبات آن ۳۵۰ سال و تلاش نسل‌ها ریاضیدان را به خود اختصاص داد و نهایتاً در سال ۱۹۹۵ توسط سر اندرو وایلز با ۱۲۹ صفحه و پس از ۷ سال کار فشرده به پایان رسید. صوری‌سازی این اثبات، یعنی تبدیل آن به زبانی که کامپیوتر بتواند گام‌به‌گام بررسی کند، سال‌ها هدف جامعه‌ی ریاضیات بوده است.
---
🤖 روش انجام و ارقام کلیدی
این پروژه با همکاری ده‌ها عامل Claude (با استفاده از مدلی قابل‌مقایسه با Claude Fable 5.1) و با بهره‌گیری از پلتفرم Prove2Me (که توسط تیان‌یی پنگ از دانشگاه کلمبیا توسعه یافته) انجام شد. فرآیند به این شکل بود:
· زمان انجام: ۱۱ روز
· تعداد خطوط کد Lean تولیدشده: ۱۳ میلیون خط
· تعداد قضایای میانی اثبات‌شده: ۳۰,۳۰۰ قضیه (که ۲۹,۵۰۰ تای آنها در اثبات نهایی استفاده شدند)
· هزینه‌ی توکن: حدود ۶ میلیارد توکن خروجی
· تعداد عامل‌های همکار: ده‌ها عامل که به‌صورت موازی و با حفظ وضعیت پروژه کار می‌کردند
پلتفرم Prove2Me با نگهداری یک گراف جهت‌دار از قضایا، به عامل‌ها امکان می‌داد تا به‌صورت موازی و بدون تداخل، بر روی بخش‌های مختلف اثبات کار کنند و از گم‌شدن وضعیت پروژه جلوگیری کند.
---
✅ تأیید صحت و اهمیت آن
اثبات تولیدشده توسط کامپایلر Lean و یک Comparator رسمی بررسی شده و صحت آن تأیید شده است. کوین بازارد، ریاضیدان برجسته‌ی مسئول پروژه‌ی صوری‌سازی این قضیه از سال ۲۰۲۴، این دستاورد را «فوق‌العاده» خوانده و تأیید کرده است که اثبات، تنها بر اساس سه اصل موضوعه‌ی استاندارد لین استوار است.
---
💡 چشم‌انداز آینده
· کاهش بار بررسی‌های انسانی: با افزایش اثبات‌های تولیدشده توسط هوش مصنوعی، صوری‌سازی خودکار می‌تواند فرآیند تأیید را که گاه سال‌ها طول می‌کشد، به شدت کاهش دهد.
· اعتماد به ریاضیات: این روش می‌تواند به کشف خطاهای بالقوه در انبوه عظیم ادبیات ریاضی کمک کند.
· دسترسی همگانی: در یک آزمایش کوچک با سه حساب کاربری شخصی Claude Max، عامل‌ها موفق شدند در تنها ۳ روز قضیه‌ی سه‌پرایم وینوگرادوف را صوری‌سازی کنند که نشان می‌دهد این قابلیت به‌زودی در دسترس عموم قرار خواهد گرفت.
محققان آنتروپیک معتقدند که به‌زودی تولید یک اثبات رسمی در کنار هر مقاله‌ی ریاضی، به یک رویه‌ی رایج تبدیل خواهد شد.
👩🏫 تعریف:
فرمالیزاسیون (یا صوری‌سازی) در ریاضیات، به فرآیند تبدیل تعاریف، قضایا و برهان‌های ریاضی از زبان معمولی انسان به یک زبان دقیق، سخت‌گیرانه و قابل‌فهم برای کامپیوتر گفته می‌شود تا هرگونه ابهام کاملاً از بین برود.
صوری‌سازی چگونه کار می‌کند؟
حذف شهود فردی: بیان غیر رسمی ریاضی به زبان طبیعی (مانند فارسی یا انگلیسی) اتکا دارد که در آن گاهی مراحل اثبات با جملاتی مثل «واضح است که...» نادیده گرفته می‌شوند. صوری‌سازی تمام گام‌های منطقی را به اصول موضوعه پایه و قوانین استنتاج صریح تجزیه می‌کند.
دستیارهای اثبات: ریاضیدانان برای نوشتن و تأیید خودکار این برهان‌ها از نرم‌افزارهایی به نام «دستیار اثبات» (یا اثبات‌کننده تعاملی قضایا) مانند Lean، Coq، Agda و Isabelle/HOL استفاده می‌کنند.
نحو (Syntax) سخت‌گیرانه: هر عبارت باید از قوانین ساختاری و برنامه‌نویسی دقیقی پیروی کند تا کامپیوتر بتواند با اطمینان ۱۰۰ درصد تضمین کند که هیچ خطای منطقی در اثبات وجود ندارد.
---
🔗 مطالعه‌ی کامل و دسترسی به اثبات:
anthropic.com/research/formalizing-fermats-last-theorem
💻 مخزن گیت‌هاب اثبات:
github.com/anthropics/fermats-last-theorem
---
#Anthropic #ریاضیات_رسمی #قضیه_آخر_فرما #هوش_مصنوعی #پیشرفت_علمی #Lean
🆔 @asrgooyeshpardaz
Anthropic
Formalizing Fermat's Last Theorem
Anthropic is an AI safety and research company that's working to build reliable, interpretable, and steerable AI systems.
❤7🔥2👍1