ونتج عن ذلك نحو 13 مليون سطر من الشيفرة البرمجية بلغة "Lean"، وحوالي 29,500 مبرهنة وسيطة، وهو ما يعادل نحو خمسة أضعاف حجم مكتبة الرياضيات الرسمية "Mathlib" بأكملها.

يُذكر أن عالم الرياضيات الفرنسي بيير دي فيرما صاغ المبرهنة في القرن السابع عشر، لكن إثباتها ظل مستعصيا لأكثر من ثلاثة قرون، إلى أن تمكن عالم الرياضيات البريطاني أندرو وايلز من إثباتها في عام 1995، بعد نحو سبع سنوات من العمل عليها بسرية.

أما الصياغة الرسمية، فتعني ترجمة البرهان الرياضي إلى شيفرة حاسوبية تتيح للحاسوب التحقق من صحة كل خطوة فيه.