# Dan Abramov ينفق نحو 40 مليار token و40 ألف دولار لبرهان رياضي واحد في Lean 4

> **المغزى:** النماذج لم تصل إلى البرهان وحدها، بل وصلت إليه مع من يعرف كيف يرى الخطأ؛ فالخبرة لم تصبح غير لازمة، بل أصبحت هي ما يضاعف الناتج.

- المصدر: المغزى (https://almaghza.com/a/2026-09-20-abramov-conway-proof-lean/)
- التاريخ: 9 ربيع الآخر - 20 سبتمبر 2026 (2026-09-20)
- القسم: ذكاء اصطناعي
- الوسوم: نماذج اللغة الكبيرة، Vibe Coding، الذكاء الاصطناعي

نشر Dan Abramov في 18 سبتمبر 2026 مقالًا بعنوان How I Vibed a Proof of Conway's Conjecture، يروي فيه تجربته في كتابة برهان لحدسية Conway المعروفة بـ refinement conjecture حول الأعداد omnific integers، مكتوبًا بالكامل في Lean 4، وهي لغة تتحقق فيها الآلة من صحة البراهين الرياضية خطوة بخطوة. واستخدم في ذلك Claude وChatGPT وCodex.

والأرقام، كما ذكرها في المقال، كبيرة: نحو 40 مليار token إجمالًا، منها نحو 210 ملايين output token. وقدّر التكلفة بأسعار الـ API الحالية بنحو 40,000 دولار، على مدى شهر تقريبًا من العمل المكثف موزع على 5 أسابيع.

أما ما حدث خلال هذه المدة فهو الجزء الأهم. في المحاولات الأولى أنتجت النماذج ما وصفه بـ "word salad"، أي مصطلحات مخترعة لا معنى لها. ثم اخترعت أطرًا نظرية كاملة لا وجود لها. والأخطر أنها بنت اعتمادات دائرية، فتثبت A باستخدام B وتثبت B باستخدام A، بينما تؤكد في كل مرة أن البرهان سليم.

وكتب Abramov في منتصف التجربة: "we do not have a proof". ثم رجع إلى رياضيين لتأكيد أخطاء مطبعية ادّعت النماذج وجودها في أوراق مرجعية، واستعان بمتخصصين للتحقق من نتائج وسيطة جديدة.

وخلاصته هو نفسه أن أكثر من سيستفيد من الذكاء الاصطناعي في هذا المجال هم الرياضيون أنفسهم.

وتقدم التجربة صورة أدق من أي عرض تسويقي. فالنموذج لم يصل إلى شيء بمفرده، بل وصل مع شخص قادر على اكتشاف الخطأ. وتطرح في الوقت نفسه سؤالًا مفتوحًا حول الكلفة: هل 40 ألف دولار لبرهان واحد رقم مرتفع، أم رخيص قياسًا بما كان يتطلبه العمل نفسه دون هذه الأدوات.

## المصادر

- [مقال Dan Abramov كاملًا بالأرقام وسجل المحاولات](https://overreacted.io/how-i-vibed-a-proof-of-conways-conjecture/)