Astăzi donăm 300.000$ lui @leanprover ca sponsor inaugural! Credem că viitorul raționamentului matematic se află în verificarea formală. Modelul nostru, Aristotel, folosește Lean pentru a elimina erorile și a verifica rezultatele. Suntem încântați să susținem instrumentele și oamenii care fac posibilă Superinteligența Matematică sigură și precisă.