مدل Astra ده نتیجه ریاضی تازه را با اثبات قابل‌بررسی در Lean 4 منتشر کرد
OpenAI نتایج یک نسخه داخلی Astra را روی ده مسئله باز ریاضی و علوم کامپیوتر نظری همراه با گواهی صوری Lean 4 منتشر کرده است.
OpenAI در ۱ اوت ۲۰۲۶ نتایجی منتشر کرد که یک نسخه داخلی از مدل Astra روی ده مسئله باز ریاضی و علوم کامپیوتر نظری به دست آورده بود. به گفته شرکت، این مسائل دست‌کم یک دهه بدون پیشرفت در نتیجه اصلی مانده بودند.
چرا Lean 4 مهم است؟
نکته فنی مهم این است که برای هر نتیجه، یک اثبات صوری (Formal Proof) به زبان Lean 4 هم منتشر شده؛ یعنی یک برنامه کامپیوتری می‌تواند درستی منطقی اثبات را دوباره بررسی کند و لازم نیست فقط به ارزیابی خود OpenAI اعتماد کرد. مجموعه منتشرشده شامل صورت قضیه‌ها، دست‌نوشته کامل، شرح استدلال مدل، کد Lean و دستور ساخت برای بررسی مستقل است.
چه نتایجی؟
- اثبات وجود گروه‌های غیر سوفیک (Non-sofic)، پرسشی که از سال ۱۹۹۹ و معرفی مفهوم سوفیک توسط میخائیل گروموف باز مانده بود.
- کران‌های بالای تازه برای بسته‌بندی کره در ابعاد بالا.
- کران‌های پایین جدید برای پیچیدگی محاسبه پرمننت با مدارهای حسابی.
- یک قضیه تکرار موازی برای بازی‌های کوانتومی دونفره.
طبق گزارش‌ها، استدلال‌های ریاضی را خود مدل تولید و صوری‌سازی کرده و پژوهشگران انسانی دست‌نوشته‌ها را برای انتشار آماده کرده‌اند. کمتر از یک روز بعد، یکی از پژوهشگران Anthropic اعلام کرد Claude Fable 5 پنج مورد از این ده نتیجه را بازتولید کرده است.
یک نکته احتیاطی هم مهم است: گواهی Lean فقط درستی منطقی اثبات را تضمین می‌کند. اینکه صورت‌بندی دقیقاً همان مسئله مورد نظر را بیان کند و نتیجه واقعاً تازه باشد، هنوز به بررسی جامعه ریاضی نیاز دارد.
