ChristianZ97/NuminaMath-LEAN-satp

NuminaMath-LEAN-satp是一个包含Lean 4形式化声明和初始证明目标状态对的数据集，主要用于SATP（Steering Aesop for Theorem Proving）的主要训练集。数据集中的每一行数据包括一个唯一的uuid、形式化声明（formal_statement）和初始证明目标状态（goal_state）。这些数据是从NuminaMath-LEAN问题池中收集的，覆盖了源数据的80.5%。数据集的处理流程包括对形式化声明的标准化处理、使用Lean工具链进行目标状态提取等步骤。数据集还提供了重新加载和使用的Python代码示例，以及相关的引用信息。

NuminaMath-LEAN-satp is a dataset containing Lean 4 formal-statement and initial proof goal_state pairs, primarily used as the main training set for SATP (Steering Aesop for Theorem Proving). Each row in the dataset includes a unique uuid, a formal_statement, and a goal_state. The data is harvested from the NuminaMath-LEAN problem pool, covering 80.5% of the source data. The datasets processing pipeline includes canonicalization of formal statements, goal state extraction using the Lean toolchain, and other steps. The README also provides Python code examples for reloading and using the dataset, along with citation information.