Monogate/petal-eml

PETAL-EML是一个教学结构化的Lean 4证明数据集，特别关注于EML（exp-minus-log）算子的形式化证明。该数据集包含了35个经过手工审核的定理，涵盖了6个教学难度级别和14个Lean文件。每个记录都包含了定理的陈述（自然语言、LaTeX和Lean 4源代码）、完整的Lean 4证明、每一步的详细解释、教学难度级别、依赖关系图以及源代码指针。数据集的设计目的是为了帮助语言模型学习如何理解和生成Lean证明，而不是作为基准测试。数据集还包含了验证工具、统计信息和详细的许可信息。PETAL-EML is a pedagogically-structured Lean 4 proof dataset focusing on the formalization of the EML (exp-minus-log) operator. The dataset includes 35 hand-audited theorems spanning 6 pedagogical difficulty lanes and all 14 Lean files in `MonogateEML/`. Each record contains the theorem statement (in natural language, LaTeX, and Lean 4 source), the full Lean 4 proof, a per-step breakdown with explanations, a lane assignment (pedagogical difficulty bucket), a dependency graph, and a source pointer. The dataset is designed as teaching material for language models to learn how to reason about Lean proofs, not as a benchmark. It also includes a validation tool, statistics, and detailed licensing information.