“The Proof in the Code” adlı icmalda “Lean” proqramının necə yarandığı və onun riyaziyyat sahəsindəki əhəmiyyəti müzakirə olunur. Başlanğıcda Microsoft tərəfindən öz məhsullarındakı proqram təminatı səhvlərini (bugları) aşkar etmək məqsədilə hazırlanmış bu proqram, gözlənilmədən riyaziyyat dünyasında böyük bir dönüş nöqtəsi yaratdı. Onun əsas funksiyası kodun doğruluğunu yoxlamaq və mürəkkəb sistemlərdəki potensial problemləri müəyyən etmək idi. “Lean” proqramının əsas xüsusiyyəti onun formal sübut sistemləri sahəsindəki imkanlarıdır. Bu sistemlər riyazi teoremlərin və məntiqi ifadələrin dəqiqliyini kompüter vasitəsilə yoxlamağa imkan verir. Proqramın bu qabiliyyəti, ənənəvi riyazi sübut proseslərindəki insan səhvlərini minimuma endirərək, daha etibarlı və dəqiq nəticələr əldə etməyə kömək edir. Bu, xüsusilə mürəkkəb riyazi problemlərin həllində və yeni teoremlərin sübutunda böyük əhəmiyyət kəsb edir. Proqramın riyaziyyatda inqilab etməsi, onun riyazi məntiqin avtomatlaşdırılması sahəsindəki potensialını ortaya qoydu. “Lean” vasitəsilə riyaziyyatçılar artıq öz sübutlarını kompüter tərəfindən yoxlatdıra bilirlər ki, bu da onların işinin dəqiqliyini və etibarlılığını artırır. Bu texnologiya, gələcəkdə riyaziyyatın inkişafına və yeni kəşflərin edilməsinə əhəmiyyətli töhfələr verə bilər. Beləliklə, Microsoft-un daxili ehtiyacları üçün yaradılan bir alət, qlobal elmi ictimaiyyət üçün dəyərli bir resursa çevrildi.