我们的 Aleph 证明代理刚刚在 PutnamBench 上获得了第一名，这是一个基于 Putnam 问题构建的基准测试——Putnam 问题是最难的大学级数学奥林匹克之一——完全通过机器检查的证明形式化，没有人类参与。Putnam 问题通常被认为比 IMO 问题更难，涵盖了广泛的主题，包括微积分、数论、群论和其他核心数学领域。 这强有力地证明了 AI 可以处理深度的多步骤推理，并提供正确性保证——我们正在使用的同种技术来验证需要形式逻辑的真实软件、硬件和科学发现。