⊕ Catalogue

Datasets

Open datasets of the lab: the knowledge graph over Mathlib, training corpora for SciLibMath / SciLibModal, full benchmark logs. Most artifacts are under open licenses with attribution; training corpora are available on request.

minif2f-50k r1

MiniF2F Bench Logs

Full logs of MiniF2F runs across four premise-retrieval pipelines. JSON-Lines, pass@1 metrics with Lean REPL verification, comparison of SciLib-GRC21 / LeanSearch / LeanFinder / LeanExplore.

488 tasks · 50 752 Lean-verified runs CC BY 4.0

slm-data-v2 v2.0

sciLibRuModal v2

Training corpus for the SciLibModal model: Mathlib mathematical objects in five modalities (EN, RU, Lean4, LaTeX, image) anchored in the SciLib ontology.

≈ 1 M multimodal records · 5 modalities on request, with attribution

mathlib-rdf 2026-04

MathLib RDF · Knowledge Graph

Knowledge graph over Mathlib statements, materialised from the SciLib ontology. Typed edges usesInType / usesInValue, domain taxonomy with provenance. The first step toward a semantic description of scientific knowledge beyond mathematics.

33.8 M triplets · 213 000+ statements · 660+ subclasses CC BY 4.0