نشرات وسيلة الإعلام التقنية Gigazine البارح (3 غشت) تدوينة، كتقول بلي تبيّن أن برهان صوري بـLean، تدار بمساعدة الذكاء الاصطناعي وكيزعم تفنيد حدسية كولاتز، ماشي صحيح.
ملاحظة: حدسية كولاتز (وكتسمّى حتى حدسية التوحيد الزوجي والفردي / حدسية 3n+1) اقترحها عالم الرياضيات الألماني لوثار كولاتز (Lothar Collatz) عام 1937، وهي مسألة رياضية بسيطة بزاف فالصياغة ديالها ولكن مازال ما تحلاتش حتى لدابا، وكتقول بلي أي عدد صحيح موجب، من بعد تكرار قواعد معيّنة عليه، غادي يرجع فالأخير دائما للعدد 1.
قواعد الحساب ديالها هي، بالنسبة لأي عدد صحيح موجب n:
إلا كان n زوجي، كنقسموه على 2 (n ÷ 2).
إلا كان n فردي، كنضربوه فـ3 ومن بعد كنزيدو 1 (3n + 1).
منين كنحصلو على عدد جديد، كنعاودو نفس الخطوات حتى تولّي النتيجة هي 1.
مثلا العدد 6:
6 عدد زوجي، وبالقسمة على 2 كنحصلو على 3
3 عدد فردي، كنضربوه فـ3 ونزيدو 1، كنحصلو على 10
10 عدد زوجي، وبالقسمة على 2 كنحصلو على 5
5 عدد فردي، كنضربوه فـ3 ونزيدو 1، كنحصلو على 16
16، بالقسمة المتتالية على 2، كيعطي 8 و4 و2 و1
المسار النهائي هو: 6 → 3 → 10 → 5 → 16 → 8 → 4 → 2 → 1.
نشر خبير التحقق الصوري Ramana Kumar مشروعا فـGitHub نهار 25 يوليوز، وقال فالأول بلي فَنّد حدسية كولاتز بمساعدة الذكاء الاصطناعي. المشروع ما عطاش مثالا مضادا محددا لعدد صحيح، وإنما برهن فـLean (وهو نظام مساعد لإثبات النظريات) على «وجود عدد ما يوصلش لـ1».
Lean هو نظام مساعد لإثبات النظريات، كيسمح للمستخدمين يكتبو الصيغ الرياضية والمنطق على شكل برامج، ومن بعد الحاسوب كيتحقق من صحة البرهان. كود Lean اللي كيكتبو المستخدم كحوّل القضايا الرياضية والبراهين لبرامج قابلة للفحص، وكتتحقق النواة من توافق الأنواع والمنطق.
ولكن من بعد، وهو كيراجع محتوى التفنيد، اكتاشف بلي هاد الطريقة كتخلي Lean يقبل بلا شروط «False» (اللي كتمثل قضية خاطئة)، وبالتالي فالكود المعني حاليا ما كيقدرش يفنّد حدسية كولاتز.
حوّل الباحث فمجال التحقق الصوري Kiran Gopinathan المشكل لشفرة صغيرة لإعادة إنتاجه، وبلّغ فريق تطوير Lean به نهار 28 يوليوز 2026.
الثغرة كانت فالنواة، فطريقة التعامل مع «الأنواع الاستقرائية المتداخلة»، وهاد الشي كان كيخليها أحيانا تتجاهل «معاملات الأنواع الشبحية» (أي المعاملات اللي ما كيبانوش مباشرة فمكوّنات بنية البيانات)، وبالتالي كانت معاملات خاصها تترفض كتدوز من التحقق. وقال مطوّر Lean Leonardo de Moura إن المشكل هو أن تنفيذ النواة ما كانش كيدير جميع الفحوصات اللازمة.
من بعد حوالي ساعة من التوصل بالتقرير، أنشأ فريق Lean طلب سحب لإصلاح المشكل، ونشر الإصدار Lean 4.32.2 نهار 28 يوليوز، واللي صلّح هاد الثغرة.