LeanTactic-40M (SchemeC)
Copyright (c) 2026 the model's authors

This release includes material derived from:

  * mathlib4  — Apache License 2.0
    https://github.com/leanprover-community/mathlib4
    All training data (proof states and tactic scripts) was mined from mathlib4 source code,
    and the 4096-token BPE vocabulary was trained on mathlib4 sources. The model's output
    distribution is therefore a statistical reflection of mathlib4's vocabulary and style.

  * LeanDojo — MIT License
    https://github.com/lean-dojo/LeanDojo
    The base split of (state, tactic) pairs comes from LeanDojo's extracted mathlib traces
    (41,944 of 87,766 declarations carry traces).

  * miniF2F — MIT License
    https://github.com/openai/miniF2F
    data/minif2f/ contains the miniF2F `valid` and `test` problem records and their .lean files.

Collected and evaluated with Lean 4.35.0-rc2 and a September 2026 mathlib4 snapshot.

If you redistribute this package or models trained on this data, keep this notice and cite
mathlib4 and LeanDojo: they supplied all of the supervision signal.