وسم

Lean

ذكاء اصطناعي

برهان رياضي كبير بمساعدة Claude وCodex يُتحقق منه في Lean، ومؤلفاه يصفان مسودته الأولى بأسوأ كتابة

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

ذكاء اصطناعي

Anthropic تصيغ برهان مبرهنة فيرما الأخيرة بلغة Lean في 11 يومًا

حين يوجد حَكَم آلي يرفض الخطأ، يستطيع الـ agent العمل أيامًا وإخراج نتيجة صحيحة. وما لا يملك حكمًا كهذا، وهو أغلب البرمجيات، ما زال يحتاج مراجعة بشرية.