| align — open post-training stack and Lean 4 prover research (Apache License 2.0) |
| Copyright 2026 the align authors |
|
|
| This product is released for open-source research under the Apache License, Version 2.0 (see LICENSE). |
|
|
| Third-party components, models and data (each under its own license; attribution required): |
|
|
| Code |
| * extras/vllm_rollout/lean_prompts.py reproduces the prompt and correction-prompt formats of |
| Goedel-Prover-V2 (Goedel-LM, https://github.com/Goedel-LM/Goedel-Prover-V2) so that evaluation matches the |
| published protocol; the reference utilities are imported from that repository at test time, not vendored. |
| * The repo-vendored Mistral-7B-v0.3 tokenizer files (align/model/checkpoint.py VENDORED_TOKENIZER_DIR) are from |
| mistralai/Mistral-7B-v0.3, Apache-2.0. |
| * Runtime dependencies: PyTorch (BSD-3-Clause), Triton (MIT), NumPy (BSD-3-Clause), safetensors (Apache-2.0). |
| Optional extras: vLLM (Apache-2.0), transformers (Apache-2.0). Lean 4, Mathlib and the Lean REPL (Apache-2.0). |
| Aeneas / Charon (Apache-2.0) in bugfind/. |
|
|
| Models |
| * Goedel-LM/Goedel-Prover-V2-8B, Apache-2.0. |
| * AI-MO/Kimina-Prover-Distill-8B, Apache-2.0. |
|
|
| Data (statement sources; per-row provenance with source id, revision and license is kept in every Problem JSONL) |
| * Goedel-LM/Goedel-Pset-v1 and HangHor/RL-Goedel-Pset-Level-4-5: MIT (informal problems from NuminaMath, Apache-2.0). |
| * SphereLab/FormalMATH-All: MIT. |
| * iiis-lean/NuminaMath-LEAN-Sol: Apache-2.0. |
| * nvidia/Nemotron-Math-Proofs-v1: CC-BY-SA-4.0 — SHARE-ALIKE: any released dataset containing rows derived from it |
| must be released under CC-BY-SA-4.0 with attribution to NVIDIA; release such rows as a separate file. |
| * Evaluation only (never trained on, decontaminated against): miniF2F (MIT), ProofNet# (MIT), MOBench, PutnamBench |
| (each under its own license, cited in the papers). |
|
|
