عامل‌های Claude در ۱۱ روز قضیه مشهور فرما را formalize کردند در یک… — VIRSUN

VIRSUN@rss_ai_ir · 10.8K subscribers Open in TelegramOpen

🧮🤖 عامل‌های Claude در ۱۱ روز قضیه مشهور فرما را formalize کردند

در یک پروژه بزرگ formal verification، عامل‌های مبتنی بر Claude نسخه‌ای ساده‌شده از اثبات Wiles برای قضیه آخر فرما را به زبان Lean تبدیل کردند.

خروجی پروژه عظیم بود: حدود ۱۳ میلیون خط کد و بیش از ۳۰ هزار قضیه میانی؛ بخش عمده آن‌ها وارد اثبات نهایی شد و کل نتیجه هم توسط کامپایلر Lean بررسی شد. Kevin Buzzard، ریاضیدانی که از ۲۰۲۴ روی formalization این قضیه کار می‌کند، نتیجه را تأیید کرده است.

نکته جالب این‌که تلاش‌های اولیه شکست می‌خوردند، چون Agentها در پروژه‌های خیلی طولانی state و هماهنگی را از دست می‌دادند. با استفاده از پلتفرم Prove2Me و نگه‌داری graph قضایا، چند Agent توانستند موازی کار کنند و افت حافظه در کار طولانی کمتر شود.

این فرایند کاملاً autonomous نبود و انسان گهگاه راهنمایی سطح‌بالا می‌داد؛ اما جهت‌گیری روشن است: در آینده، AI می‌تواند بخش بزرگی از formalization و verification اثبات‌های ریاضی را به‌صورت ماشینی انجام دهد.
https://www.anthropic.com/research/formalizing-fermats-last-theorem

@rss_ai_ir
❤️ حمایت از کانال:
https://daramet.com/Virsun

#Claude #Anthropic #Lean #FormalVerification #Mathematics #Fermat #AIAgent #TheoremProving #هوش_مصنوعی

t.me/rss_ai_ir/5323 Translate