今天我們將捐贈 $300,000 給 @leanprover 作為首位贊助商！ 我們相信數學推理的未來在於形式驗證。我們的模型 Aristotle 使用 Lean 來消除錯誤並驗證結果。我們很高興能支持那些使安全、準確的數學超智能成為可能的工具和人員。