Datasets · SciLib

⊕ 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.

{# Декоративный фоновый знак — только короткий symbol (один глиф), длинные LaTeX-формулы из artifact.formula не используются: они теснили контент и ломали выравнивание. #}
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
{# Декоративный фоновый знак — только короткий symbol (один глиф), длинные LaTeX-формулы из artifact.formula не используются: они теснили контент и ломали выравнивание. #}
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
{# Декоративный фоновый знак — только короткий symbol (один глиф), длинные LaTeX-формулы из artifact.formula не используются: они теснили контент и ломали выравнивание. #}
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