ProofNet

ProofNet 是一个用于本科数学的自动形式化和形式证明的基准。包含 371 个示例，每个示例包括一个 Lean 3 中的形式定理陈述、一个自然语言定理陈述和一个自然语言证明。这些问题主要来自流行的本科纯数学教材，涵盖实分析、复分析、线性代数、抽象代数和拓扑等主题。