uw-math-ai/grothendieck-vanishing-logs

该数据集包含一个LLM辅助形式化过程中的处理数据和专家代码审查，该过程使用Lean 4对Noetherian拓扑空间上阿贝尔群层的Grothendieck消失定理进行了形式化。形式化工作由Claude Code和Codex代理完成，并使用Aristotle证明器处理有界引理。数据集还包括两次专家审查（状态A和状态B）以及结构化过程日志，用于前后比较。This dataset contains processing data from an LLM-assisted formalization process and expert code reviews. The formalization work targeted the Grothendieck Vanishing Theorem for sheaves of abelian groups on Noetherian topological spaces, which was conducted using Lean 4. The formalization was completed by Claude Code and Codex agents, with the Aristotle prover utilized to handle bounded lemmas. The dataset also includes two rounds of expert reviews (State A and State B) as well as structured process logs for pre- and post-comparison.