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