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