形式验证在大规模上实现信任

现在我们已经有117个正式的厄尔多斯问题解决方案，比四个月前的个位数有所增加。 超过四分之三的解决方案是由亚里士多德提供的。

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