يُثبت هذا البحث أن أي عدد صحيح غير سالب يمكن كتابته بالصيغة التالية $x(x+1)/2 + y(3y+1)/2 + z(5z+1)/2, qquad x,y,z in mathbb{N}.$x(x+1)/2+y(3y+1)/2+z(5z+1)/2,qquadx,y,zinmathbbN. وبذلك يُحسم التخمين المسجل تحت الرقم OEIS A287616. وقد تمت صياغة جميع أجزاء البرهان شكلياً في Lean 4، باستثناء نتيجتين: مبرهنة مستشهدة من مصدر خارجي، وبيان تم التحقق منه باستخدام الحساب الرمزي. وقد تم توليد كل من البرهان المصاغ باللغة الطبيعية والترميز الشكلي في Lean بواسطة فريق MechMath Agent Team الذي طوره المؤلفون.