Extensively annotated Isabelle source code, suitable for pretraining, about 500M tokens in Qwen3's tokenizer.
Data source: Isabelle/HOL + AFP 2025-02-12. Cases from the PISA benchmark are removed.
Example:
lemma (in group) diff_neutralizes: ✐‹contributor ‹Paulo EmÃlio de Vilhena››
assumes "subgroup H G" "R ∈ rcosets H"
shows "⋀r1 r2. ⟦ r1 ∈ R; r2 ∈ R ⟧ ⟹ r1 ⊗ (inv r2) ∈ H"
proof (-)
(
goal: ‹⋀r1 r2. ⟦r1 ∈ R; r2 ∈ R⟧ ⟹ r1 ⊗ inv r2 ∈ H›)
fix r1 and r2
assume r1: "r1 ∈ R" and r2: "r2… See the full description on the dataset page:
https://huggingface.co/datasets/ANTPG/annotated-isabelle.
