FrancoisMichelon/lean_rocq

Lean & Rocq Formal Proof Datasets This repository contains curated datasets of formal proof code and documentation from the Lean and Rocq theorem prover ecosystems, hosted on Hugging Face Hub. HF Repository: FrancoisMichelon/lean_rocq Overview The datasets combine multiple sources: Repository source code: .v (Rocq/Coq) and .lean (Lean 4) files from major libraries Documentation: Extracted HTML pages from official docs with structured metadata Educational… See the full description on the dataset page: https://huggingface.co/datasets/FrancoisMichelon/lean_rocq.