---
license: apache-2.0
tags: [lean4, theorem-proving, post-training, grpo, code]
---
# align: open post-training stack and Lean 4 prover research (code)

Snapshot of 2026-10-19:
- `code/`: the working tree at the commit named in `COMMIT`.
- `align.bundle`: a git bundle with the full history. Restore it with `git clone align.bundle align`.

Data is at https://huggingface.co/datasets/viai957/lean-prover-data.

The code is licensed Apache-2.0 (see `code/LICENSE`); third-party attributions are in `code/NOTICE`.
The pre-registration is `code/docs/PREREG_SOTA.md`, OpenTimestamps-stamped under `code/docs/evidence/prereg/`.

**Status:** Phase 0, with no trained checkpoint yet.

**Model revisions used:** `code/docs/evidence/model_revisions_deleted_2026-10-19.txt`.