今天我们将作为首个赞助商捐赠30万美元给@leanprover！ 我们相信数学推理的未来在于形式验证。我们的模型Aristotle使用Lean来消除错误并验证结果。我们很高兴能支持那些使安全、准确的数学超级智能成为可能的工具和人。