Claude قضیه آخر فرما را در Lean رسمی‌سازی کرد

Anthropic اخیراً یک وظیفه پژوهشی عظیم را به پایان رساند. یک مدل داخلی به مدت ۱۱ روز کار کرد تا قضیه آخر فرما را با استفاده از زبان اثبات Lean 4 رسمی‌سازی کند.

این یک کشف ریاضی جدید نیست. اندرو وایلز این قضیه را در سال ۱۹۹۵ اثبات کرد. کاری که Anthropic انجام داد، ترجمه آن اثبات موجود به کد بود. این کار به کامپیوتر اجازه می‌دهد تا هر مرحله منطقی را با اطمینان کامل بررسی کند.

مقیاس این پروژه عظیم است: • مدل ۱۳ میلیون خط کد Lean تولید کرد. • ۳۰,۳۰۰ قضیه میانی را اثبات کرد. • تقریباً از ۶ میلیارد توکن خروجی استفاده کرد.

مدل عمدتاً به تنهایی کار کرد. انسان‌ها فقط گاهی اوقات دستورالعمل‌های سطح بالا ارائه دادند. این فرآیند در نیمه‌شب، زمانی که هیچ‌کس نظاره‌گر نبود، به پایان رسید. سیستم موفقیت را به‌طور خودکار ثبت کرد.

دو نکته مهم که باید به آن‌ها توجه کرد: ۱. این مدل یک ابزار پژوهشی داخلی است. شما هنوز نمی‌توانید از طریق API به آن دسترسی داشته باشید. این مدل با مدل‌های Claude که امروزه استفاده می‌کنید، متفاوت است. ۲. ارزش واقعی برای توسعه‌دهندگان در لایه هماهنگ‌سازی به نام Prove2Me نهفته است.

Prove2Me یک ابزار متن‌باز است. این ابزار از یک گراف وابستگی برای مدیریت وظایف استفاده می‌کند. به جای یک چک‌لیست ساده، نقشه‌ای از نحوه اتصال اثبات‌ها به یکدیگر ایجاد می‌کند.

این ساختار دو مشکل بزرگ را در جریان‌های کاری عامل‌ها (agent workflows) حل می‌کند:

  • از انجام کار یکسان توسط چندین عامل جلوگیری می‌کند.
  • به عامل‌ها یک حافظه مشترک می‌دهد تا هدف اصلی را فراموش نکنند.

بیشتر جریان‌های کاری عامل‌ها شکست می‌خورند زیرا با گذشت زمان، زمینه (context) را از دست می‌دهند. استفاده از یک گراف خارجی و مشترک به جای یک پنجره چت طولانی، باعث می‌شود وظیفه در مسیر درست باقی بماند.

اگر جریان‌های کاری عامل‌ها را می‌سازید، باید معماری Prove2Me را مطالعه کنید. حتی اگر از مدل‌های پژوهشی Anthropic استفاده نمی‌کنید، روش هماهنگی آن‌ها برای وظایف، الگویی برای کارهای بلندمدت است.

منبع: https://dev.to/raxxostudios/claude-just-formalized-fermats-last-theorem-in-lean-3p36

جامعه یادگیری اختیاری: https://t.me/GyaanSetuAi