گوگل دیپ‌مایند (Google DeepMind) نتیجه‌های سیستمِ AlphaProof Nexus را در مجله‌ی علمیِ Science منتشر کرد؛ خبری که روز ۱۲ اکتبر ۲۰۲۶ (۲۰ مهر ۱۴۰۵) بازتاب گسترده‌ای داشت. این سیستم ۹ مسئله‌ی باز از مجموعه‌ی مشهورِ «مسئله‌های اردوش» را حل کرده که دو تا از آن‌ها ۵۶ سال بی‌جواب مانده بودند. مهم‌تر از خودِ عدد، این است که کار پیش از انتشار، داوریِ علمی (peer review) شده است.
AlphaProof Nexus چیست؟
AlphaProof Nexus یک «ایجنتِ ریاضی» است که دو چیز را کنارِ هم می‌گذارد: یک مدلِ زبانیِ بزرگ که اثبات را می‌نویسد، و زبانِ Lean که درستیِ هر قدمِ اثبات را با کامپیوتر وارسی می‌کند. Lean یک «اثبات‌گرِ رسمی» است؛ یعنی اگر حتی یک قدم از استدلال غلط باشد، اثبات را قبول نمی‌کند. به این ترتیب دیگر لازم نیست به حرفِ مدل اعتماد کنیم؛ هر اثباتی که از Lean بگذرد، از نظرِ منطقی درست است.
به گزارشِ The Decoder، این سیستم بر پایه‌ی Gemini 3.1 Pro ساخته شده است. مدل یک پیش‌نویسِ اثبات به زبانِ Lean می‌نویسد، Lean آن را وارسی می‌کند و پیام‌های خطایش راهنمای تلاشِ بعدی می‌شود. برای زیرمسئله‌های سخت‌تر، سیستم می‌تواند از AlphaProof، ابزارِ تخصصیِ اثبات‌سازیِ دیپ‌مایند، کمک بگیرد. جالب اینکه به گفته‌ی دیپ‌مایند، آن ۹ مسئله‌ی اردوش حتی بدونِ AlphaProof و فقط با مدلِ زبانی و بازخوردِ Lean هم حل شدند، هرچند برای سخت‌ترین‌ها هزینه‌ی بیشتری داشت.
چه مسئله‌هایی حل شد؟
| بخش | نتیجه |
|---|---|
| مسئله‌های بازِ اردوش | ۹ مسئله از ۳۵۳ مسئله‌ای که امتحان شد؛ دو مسئله ۵۶ سال باز بود |
| حدس‌های پایگاهِ دنباله‌های عددی (OEIS) | ۴۴ حدس از ۴۹۲ حدسِ باز |
| هندسه‌ی جبری | جوابِ یک پرسشِ ۱۵ ساله درباره‌ی «تابع‌های هیلبرت» |
| بهینه‌سازی | بهترکردنِ یک کرانِ شناخته‌شده در بهینه‌سازیِ min-max که در آموزشِ برخی مدل‌های هوش مصنوعی هم کاربرد دارد |
«مسئله‌های اردوش» فهرستی از صدها پرسشِ ریاضی است که پال اردوش، ریاضیدانِ پرکارِ مجارستانی، در طولِ عمرش مطرح کرد. بسیاری از آن‌ها ظاهرِ ساده‌ای دارند ولی دهه‌ها ریاضیدان‌ها را سرگرم کرده‌اند. به همین دلیل این فهرست به محکی محبوب برای سنجشِ توانِ هوش مصنوعی در ریاضی تبدیل شده است.
البته عدد را باید در اندازه‌ی خودش دید: ۹ از ۳۵۳ یعنی حدودِ ۲٫۵ درصد. یعنی سیستم هنوز بیشترِ مسئله‌ها را حل نمی‌کند. ولی هر کدام از این ۹ مسئله، چیزی است که ریاضیدان‌ها سال‌ها رویش کار کرده بودند و هر اثبات با کامپیوتر وارسی شده است. طبقِ پیش‌نویسِ مقاله، هزینه‌ی پردازش برای هر مسئله فقط چند صد دلار بوده است. اثبات‌ها و توضیحِ برخی از آن‌ها هم در مخزنِ عمومیِ دیپ‌مایند در GitHub منتشر شده است.
چرا داوریِ علمی این‌قدر مهم است؟
چند روز پیش OpenAI صدها نتیجه‌ی ریاضیِ ساخته‌ی هوش مصنوعی را مستقیم در GitHub گذاشت و بحثِ زیادی میانِ ریاضیدان‌ها راه انداخت؛ ماجرای آن را در خبرِ انتشارِ ۳۷۲ نتیجه‌ی ریاضیِ OpenAI خوانده‌ایم. دیپ‌مایند راهِ دیگری رفته و کارش را برای داوری به یک مجله‌ی معتبر فرستاده است. داوری یعنی متخصصانِ مستقل پیش از انتشار، روش و ادعاها را بررسی کرده‌اند. برای ادعایی به این بزرگی، این قدم اعتبارِ نتیجه را خیلی بالا می‌برد.
نکته‌ی دیگر این است که نتیجه بیشتر از هر چیز، قدرتِ ترکیبِ «مدلِ زبانی + وارسی‌کننده‌ی رسمی» را نشان می‌دهد. مدل‌های زبانی گاهی با اعتمادبه‌نفس حرفِ غلط می‌زنند؛ ولی وقتی یک وارسی‌کننده‌ی سخت‌گیر کنارشان باشد، می‌شود از خلاقیتشان استفاده کرد بی‌آنکه نگرانِ خطا بود. همین ایده کم‌کم در برنامه‌نویسی و علوم دیگر هم به کار می‌رود.
این خبر برای دانشجو و پژوهشگرِ فارسی‌زبان چه معنایی دارد؟
AlphaProof Nexus یک ابزارِ عمومی نیست که بشود ثبت‌نام کرد و از آن استفاده کرد. ولی پیامش روشن است: هوش مصنوعی دارد از «کمک در حلِ تمرین» به «همکار در پژوهش» نزدیک می‌شود. برای دانشجوهای ریاضی و رشته‌های فنی، یادگرفتنِ ابزارهایی مثلِ Lean می‌تواند در سال‌های آینده مهارتِ ارزشمندی باشد.
اگر می‌خواهید همین حالا از هوش مصنوعی برای فهمیدنِ اثبات‌ها، حلِ مسئله یا توضیحِ مفاهیمِ ریاضی کمک بگیرید، در هوش‌نو می‌توانید با Gemini، Claude، GPT و DeepSeek به فارسی گفت‌وگو کنید. یک ترفندِ مفید: از مدل بخواهید هر قدمِ استدلال را جدا بنویسد و بعد از مدلِ دیگری بخواهید همان را وارسی کند. برای انتخابِ مدلِ مناسب، مقایسه‌ی Claude با ChatGPT و Gemini را ببینید؛ تازه‌ترین نسلِ مدل‌های گوگل را هم در خبرِ Gemini 4 Argon معرفی کرده‌ایم. فهرستِ کاملِ امکانات در ابزارهای هوش‌نو است.
سؤالات متداول
AlphaProof Nexus چند مسئله‌ی اردوش را حل کرد؟
۹ مسئله از ۳۵۳ مسئله‌ی بازی که امتحان شد؛ دو تا از آن‌ها ۵۶ سال بی‌جواب بودند.
از کجا معلوم است اثبات‌ها درست‌اند؟
همه‌ی اثبات‌ها به زبانِ Lean نوشته و با کامپیوتر وارسی شده‌اند و مقاله هم پیش از انتشار در Science داوری شده است.
آیا می‌توانم از AlphaProof Nexus استفاده کنم؟
نه، این یک سیستمِ پژوهشیِ دیپ‌مایند است. فقط اثبات‌ها و نتیجه‌ها به‌صورتِ عمومی منتشر شده‌اند.
