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 materials: Course materials and tutorials for both languages
• —Opam packages: .v files from rocq packages

This is ideal for:

• —Training language models on formal proof code
• —Fine-tuning models for theorem proving tasks
• —Analyzing formal proof patterns and best practices
• —Building proof assistants and IDE tools

Dataset Contents

1. Repository Files (repos_files.jsonl)

Complete source code from major Lean and Rocq libraries.

Included repositories (27 total):

Rocq/Coq projects:

• —math-comp, analysis, Coq-Combi, finmap, multinomials, coq-robot
• —mathcomp-extra, fourcolor, infotheo, CoqPrime, HB, category-theory
• —algebra-tactics, odd-order, Abel, rocq, real-closed, cad, bigenough
• —dioid, tutorial_material

Lean 4 projects:

• —mathlib4, lean4, lean-liquid, mathematics_in_lean, aesop, batteries
• —lean-perfectoid-spaces

Format: One JSON object per line

{
  "source": "math-comp/src/algebra/matrix.v",
  "text": "... full source code ...",
  "language": "rocq"
}

2. Documentation

Multiple doc files extracted from official sources:

rocq-prover.org_doc.jsonl

Official Rocq/Coq documentation including:

• —Language reference
• —Standard library docs
• —API documentation
• —Best practices guides

lean-lang.org_doc.jsonl

Official Lean 4 language documentation

leanprover-community.github.io_doc.jsonl

Community Lean resources and tutorials

hrmacbeth.github.io_doc.jsonl

Educational Lean materials

Format: One JSON object per documentation page

{
  "source": "docs/en/reference/expressions.html",
  "text": "... cleaned and structured documentation ...",
  "language": "rocq"
}

3. Course Materials

Structured course content from Software Foundations and related educational resources:

• —lf-current.jsonl - Logical Foundations
• —plf-current.jsonl - Programming Language Foundations
• —qc-current.jsonl - Quick Coq
• —secf-current.jsonl - Separation and Concurrency
• —slf-current.jsonl - Software Foundations in Lean
• —vc-current.jsonl - Verified Computing
• —vfa-current.jsonl - Verified Functional Algorithms

4. PDF Materials

Extracted from textbooks:

• —book.jsonl - Main formal methods textbook
• —pnp.jsonl - Proofs and Proofs textbook

5. Opam packages

Opam packages list:

• —coq-actuary.2.6
• —coq-atbr.8.20.0
• —coq-color.1.8.5
• —coq-compcert.3.16
• —coq-coqeal.2.1.1
• —coq-coqtail.8.20
• —coq-coquelicot.3.4.4
• —coq-corn.9.0.0
• —coq-ext-lib.0.13.0
• —coq-extructures.0.5.0
• —coq-fcsl-pcm.2.2.0
• —coq-flocq.4.2.1
• —coq-geocoq.2.5.0
• —coq-geocoq-algebraic.2.5.0
• —coq-geocoq-axioms.2.5.0
• —coq-geocoq-coinc.2.5.0
• —coq-geocoq-elements.2.5.0
• —coq-geocoq-main.2.5.0
• —coq-geocoq-pof.2.5.0
• —coq-graph-theory.0.9.7
• —coq-high-school-geometry.8.16.0
• —coq-hott.9.0
• —coq-iris.4.4.0
• —coq-itree.5.2.1
• —coq-karp-miller.1.1
• —coq-kruskal-almostfull.2.0
• —coq-kruskal-fan.2.0
• —coq-kruskal-finite.2.0
• —coq-kruskal-higman.2.0
• —coq-kruskal-theorems.2.0
• —coq-kruskal-trees.2.0
• —coq-kruskal-veldman.2.0
• —coq-library-fol.1.0+8.20
• —coq-library-undecidability.1.1.2+8.20
• —coq-libvalidsdp.1.1.1
• —coq-math-classes.9.0.0
• —coq-mk-choice-axiom-and-equivalent-propositions.1.0.0
• —coq-mk-reals-axioms.1.0.0
• —coq-mmaps.1.1
• —coq-ordinal.0.5.6
• —coq-pil.1.0.1
• —coq-plouffe.1.5.0
• —coq-quantumlib.1.8.0
• —coq-quickchick.2.1.1
• —coq-reglang.1.2.2
• —coq-relation-algebra.1.8.0
• —coq-relation-extraction.8.8.0
• —coq-sail.0.20.1
• —coq-ssprove.0.3.0
• —coq-stdpp.1.12.0
• —coq-trocq-hott.0.2.0
• —coq-trocq-hott-examples.0.2.0
• —coq-trocq-std.0.2.0
• —coq-trocq-std-examples.0.2.0
• —coq-unimath.20250923
• —coq-zorns-lemma.10.2.0
• —rocq-metarocq.1.4.1+9.1
• —rocq-num-analysis-algebra.2.1.0
• —rocq-num-analysis-fem.2.1.0
• —rocq-num-analysis-lax-milgram.2.1.0
• —rocq-num-analysis-lebesgue.2.1.0
• —rocq-num-analysis-subset.2.1.0
• —rocq-ollibs.2.1.1
• —rocq-pi-agm.1.2.9
• —rocq-relation-algebra.1.8.0
• —rocq-rouche-capelli.0.2.0

Data Schema

Repository, Opam packages & Course Files

{
  "source": "string (file path or identifier)",
  "text": "string (complete source code or content)",
  "language": "rocq" | "lean"
}

Documentation Files

{
  "source": "string (relative URL path)",
  "text": "string (cleaned and structured documentation text)",
  "language": "rocq" | "lean"
}

Note: Raw HTML extraction includes metadata in intermediate JSON files under raw_doc_pages/, but the final .jsonl files contain only the cleaned, structured text suitable for training.

Loading & Usage

Quick Start (Hugging Face Datasets Library)

from datasets import load_dataset

# Load the full merged dataset
dataset = load_dataset("FrancoisMichelon/lean_rocq")

# Load specific splits (if available)
rocq_code = load_dataset("FrancoisMichelon/lean_rocq", split="rocq_repos")
lean_code = load_dataset("FrancoisMichelon/lean_rocq", split="lean_repos")
docs = load_dataset("FrancoisMichelon/lean_rocq", split="documentation")

Filter by Language

# Rocq/Coq only
rocq_dataset = dataset.filter(lambda x: x["language"] == "rocq")

# Lean 4 only
lean_dataset = dataset.filter(lambda x: x["language"] == "lean")

Iterate Over Data

from datasets import load_dataset

dataset = load_dataset("FrancoisMichelon/lean_rocq")

for example in dataset.take(10):
    print(f"Source: {example['source']}")
    print(f"Language: {example['language']}")
    print(f"Text length: {len(example['text'])} chars\n")

For Training

from transformers import AutoTokenizer

tokenizer = AutoTokenizer.from_pretrained("mistral-7b")
dataset = load_dataset("FrancoisMichelon/lean_rocq")

def tokenize(example):
    return tokenizer(example["text"], truncation=True, max_length=4096)

tokenized = dataset.map(tokenize, batched=True)

Dataset Statistics

Note: Exact counts depend on extraction completeness and update frequency.

Extraction & Preprocessing

Source Processing

1. 1.Repository files: Walk directory trees, extract .v (Rocq) and .lean (Lean 4) files with multiple encoding fallbacks (UTF-8 → Latin-1 → Windows-1252)

1. 1.Documentation:
2. 2.Parse HTML with BeautifulSoup and html5lib
3. 3.Extract headings, paragraphs, code blocks, lists, and tables
4. 4.Clean whitespace (collapse multiple newlines, normalize spaces)
5. 5.Remove navigation, footers, scripts, styles
6. 6.Preserve structured metadata (breadcrumbs, block types)

1. 1.Merge: All individual JSONL files are merged into a single merged.jsonl containing all records

Language Detection

Inferred from:

• —File extension (.v → Rocq, .lean → Lean)
• —Source directory name
• —Explicit language tags in extraction metadata

Updates & Maintenance

This dataset is periodically updated to include:

• —New releases from Rocq/Coq and Lean ecosystems
• —Updated documentation from official sources
• —Additional course materials and tutorials

Last updated: Check the dataset card on Hugging Face Hub for the latest timestamp.

Citation

If you use this dataset, please cite:

@dataset{michelon2025lean_rocq,
  title={Lean & Rocq Formal Proof Datasets},
  author={Michelon, Fran\c{c}ois},
  year={2025},
  howpublished={\url{https://huggingface.co/datasets/FrancoisMichelon/lean_rocq}}
}

License

This dataset aggregates content from multiple sources under their respective licenses:

• —Rocq/Coq repositories: Various (check individual repo licenses)
• —Lean 4 repositories: Apache 2.0 (mathlib4, lean4)
• —Official documentation: Creative Commons or project-specific licenses
• —Educational materials: Varies by source

Compiled dataset: Made available for research and educational purposes. Respect the original source licenses when using individual components.

Troubleshooting

Dataset not found

Ensure your huggingface_hub is updated:

pip install --upgrade huggingface-hub datasets

Authentication issues

Log in to Hugging Face:

huggingface-cli login

Memory issues when loading full dataset

Load with streaming:

dataset = load_dataset("FrancoisMichelon/lean_rocq", streaming=True)

Or load splits individually:

# Load only documentation
docs = load_dataset("FrancoisMichelon/lean_rocq", split="documentation")

Contributing

Found missing repositories, documentation, or errors? Open an issue or pull request on the project repository.

Related Resources

• —Rocq Official Site
• —Lean 4 Documentation
• —mathlib4 Repository
• —Software Foundations

Contact

For questions or suggestions about this dataset, please contact the maintainers or open an issue on the Hugging Face Hub.