Idag donerar vi 300 000 dollar till @leanprover som den första sponsorn! Vi tror att framtiden för matematisk logik ligger i formell verifiering. Vår modell, Aristoteles, använder Lean för att eliminera fel och verifiera resultat. Vi är glada att stödja de verktyg och de människor som gör säker, korrekt matematisk superintelligens möjlig.