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