OBT

该数据集是一个经过NL-FL对齐和自举的集合，其中包含了通过一种自举方法生成的定理，该方法将自然语言证明整合到Lean4代码中。该数据集是使用Gemini-1.5-Pro-0409来编写定理的自然语言以及执行NL-FL自举生成的。数据集规模包含106,852个定理。其任务是针对基于Lean4语句和自然语言语句的数学问题生成完整的Lean4证明。

This dataset is a bootstrapped collection aligned between natural language (NL) and formal language (FL). It contains theorems generated via a bootstrapping method that integrates natural language proofs into Lean4 code. Developed using Gemini-1.5-Pro-0409, which was employed to craft the natural language descriptions of the theorems and implement the NL-FL bootstrapping workflow, the dataset comprises a total of 106,852 theorems. Its core task is to generate complete formal Lean4 proofs for mathematical problems based on both Lean4 formal statements and natural language statements.