# OpenAI تعلن عن نموذج Astra بعد نتائج في 10 مسائل رياضية مفتوحة

> **المغزى:** ما يجعل الادعاء قابلًا للتصديق ليس النموذج بل Lean: نظام يتحقق آليًا من كل خطوة في البرهان، فلا تمر الهلوسة مهما كانت مقنعة.

- المصدر: المغزى (https://almaghza.com/a/2026-08-03-openai-astra-math-lean/)
- التاريخ: 20 صفر - 3 أغسطس 2026 (2026-08-03)
- القسم: ذكاء اصطناعي
- الوسوم: OpenAI، Lean، نماذج اللغة الكبيرة، الذكاء الاصطناعي

أعلنت OpenAI في 2 أغسطس 2026 عن نموذج لم يصدر بعد باسم Astra، ووصفته بأنه "نموذجنا الكبير القادم". وجاء الإعلان بعد أن توصلت نسخة داخلية منه إلى نتائج في 10 مسائل مفتوحة في الرياضيات وعلوم الحاسوب النظرية.

ومن بين هذه المسائل نفي حدسية Connes، وإثبات حدسية Ehrhart، وأول تحسين منذ عام 1978 للحد الأعلى لكثافة رص الكرات في الأبعاد العالية. وبحسب الشركة، كانت الـ tokens المستهلكة في ذلك ستكلف نحو 2,000 دولار بأسعار الـ API الحالية.

لكن ما يجعل هذا الادعاء قابلًا للتصديق أصلًا ليس النموذج، بل Lean. وهو نظام لكتابة البراهين الرياضية بلغة تفهمها الآلة، ثم تتحقق الآلة من كل خطوة فيها. فإذا وُجدت قفزة غير مبررة في البرهان لا يقبلها النظام، ولا مكان فيه لعبارة "هذه الخطوة واضحة". وبحسب ما أُعلن، صيغت البراهين في Lean وجرى التحقق منها.

وهذا يعني أن النموذج قد يهلوس كما يشاء، لكن الهلوسة لا تمر. فالحكم هنا ليس رأي بشر ولا ثقة في شركة، بل نظام يجيب بنعم أو لا.

وترسم الحالة خطًا واضحًا بين نوعين من المجالات. المجالات التي تملك طريقة آلية للتحقق من الإجابة، كالرياضيات والبرمجة والتشفير، يمكن أن تتقدم فيها النماذج بسرعة كبيرة. أما المجالات التي تُقيَّم إجاباتها بحكم بشري، كالتصميم والاستراتيجية والكتابة، فتبقى معتمدة على البشر بدرجة أكبر.

ويبقى أن النتائج لم تخضع بعد لمراجعة الأقران، وأن النموذج لم يصدر. فما أُعلن حتى الآن هو ما تقوله الشركة عن نموذجها.

## المصادر

- [تقرير BleepingComputer عن Astra](https://www.bleepingcomputer.com/news/artificial-intelligence/openai-teases-astra-its-next-major-ai-model-after-it-solves-10-long-standing-math-problems/)
- [تفاصيل المسائل العشر في The Decoder](https://the-decoder.com/openai-announces-its-next-major-model-astra-by-dropping-ten-previously-unsolved-math-solutions/)
- [تغطية TNW](https://thenextweb.com/news/openai-astra-model-ten-math-proofs-non-sofic-groups)
- [الموقع الرسمي لنظام Lean](https://lean-lang.org/)