使用场景

在 miniF2F 基准测试中，Goedel-Prover 达到了 57.6% 的成功率，显著高于其他开源模型。

在 PutnamBench 排行榜中，Goedel-Prover 成功解决了 7 个问题，位居榜首。

为 Lean Workbook 生成了 29.7K 个形式化证明，几乎翻倍于此前的工作成果。

产品特色

将自然语言数学问题翻译为形式化语言（Lean 4）

生成高质量的形式化证明

支持多数据集的性能评估

提供开源模型和数据集，便于研究和扩展

在多个基准测试中表现优异，如 miniF2F 和 PutnamBench

支持多 GPU 并行推理，提升计算效率

使用教程

1. 克隆仓库：`git clone --recurse-submodules https://github.com/Goedel-LM/Goedel-Prover.git`

2. 安装依赖：`pip install -r requirements.txt`

3. 构建 Lean 4 和 mathlib4：`cd mathlib4 && lake build`

4. 测试安装：运行 `python prover/lean/verifier.py` 确保环境正常

5. 运行推理：使用 `sh eval/eval.sh` 脚本，指定数据集、模型路径和输出目录等参数