lean-dojo Retrieval-Augmented Theorem Provers for Lean
active 2023-08-15 → 2026-05-09 (UTC)
Activity over time
Daily event counts in the loaded window
Line chart, 999 days from 2023-08-15 to 2026-05-09. Pushes: 80 total, peak 4 in a day. Pull requests: 33 total, peak 4 in a day. Issues: 39 total, peak 3 in a day. Comments: 76 total, peak 5 in a day. Stars: 200 total, peak 5 in a day.
- Pushes
- Pull requests
- Issues
- Comments
- Stars
Stars, PRs, issues and forks are under-captured in the later part of this window. GH Archive progressively stopped capturing non-push events during 2026 — −95% or worse by the end of the window. Every series here except Pushes fades for that reason, so a decline above reflects the archive, not this repository. Pushes stay reliable throughout, so read them, and the contributor counts derived from them, as the real signal. Data health has the measurements.
Top contributors
Pushes, PRs, issues, reviews and comments — stars and forks excluded, so this is contribution rather than popularity
| Contributor | Contributions | Pushes | PRs | Comments |
|---|---|---|---|---|
| yangky11 | 155 | 78 | 21 | 41 |
| irene622 | 28 | 0 | 4 | 12 |
| Yingjia-Wan | 6 | 0 | 0 | 5 |
| zoryzhang | 5 | 0 | 0 | 3 |
| mnluzimu | 4 | 0 | 0 | 2 |
| AG161 | 3 | 0 | 0 | 1 |
| j991222 | 3 | 0 | 0 | 1 |
| Peiyang-Song | 3 | 1 | 2 | 0 |
| hongjin-su | 3 | 0 | 0 | 1 |
| huolongguo1O | 3 | 0 | 2 | 1 |
| Sara-Rajaee | 3 | 0 | 0 | 1 |
| albertqjiang | 3 | 0 | 1 | 1 |
| ketchupfan | 2 | 0 | 0 | 1 |
| yifan123 | 2 | 0 | 0 | 1 |
| m50047181 | 2 | 0 | 0 | 1 |
| euclidgame | 2 | 0 | 1 | 1 |
| Purewhite2019 | 1 | 0 | 0 | 1 |
| mikeljl | 1 | 0 | 0 | 0 |
| luan-xiaokun | 1 | 0 | 0 | 0 |
| matt-seb-ho | 1 | 0 | 1 | 0 |
Recent activity
Latest issues, pull requests and releases
- Issue#76yangky112025-08-30 14:42Many missing premises while training premise selector.
- Issue#80bogedy2025-08-22 13:19running eval correctly?
- Issue#78mikeljl2025-05-13 09:21Question about released checkpoint split strategy
- Issue#77yangky112025-03-24 19:31Does the index need to be rebuilt every time I run the retriever?
- Issue comment#77milangritta2025-03-17 14:01Does the index need to be rebuilt every time I run the retriever?
- Issue#77m500471812025-03-14 15:51Does the index need to be rebuilt every time I run the retriever?
- Issue comment#76m500471812025-03-14 15:50Many missing premises while training premise selector.
- Issue comment#76ketchupfan2025-03-05 10:25Many missing premises while training premise selector.
- Issue#73yangky112025-03-05 02:51Evaluation on multiple GPUs
- Issue comment#76yangky112025-03-05 02:50Many missing premises while training premise selector.
- Issue#76ketchupfan2025-02-19 16:44Many missing premises while training premise selector.
- Pull request#75yangky112025-01-30 13:34
- Issue comment#75euclidgame2025-01-29 20:35Fix Missing `TimeoutError` by Replacing with `DojoTacticTimeoutError`
- Pull request#75euclidgame2025-01-29 20:34
- Issue comment#72AG1612024-09-27 18:50"ValueError: Tensors must be contiguous" When re-running experiments
- Issue#72AG1612024-09-27 18:50"ValueError: Tensors must be contiguous" When re-running experiments
- Issue comment#72yangky112024-09-24 02:21"ValueError: Tensors must be contiguous" When re-running experiments
- Issue comment#73yangky112024-09-24 00:57Evaluation on multiple GPUs
- Issue#73ezhang74232024-09-22 20:36Evaluation on multiple GPUs
- Issue#71Sara-Rajaee2024-09-19 10:11Deepspeed checkpoint error when using the released Huggingface checkpoints
- Issue comment#71Sara-Rajaee2024-09-19 10:11Deepspeed checkpoint error when using the released Huggingface checkpoints
- Issue#72AG1612024-09-12 21:22"ValueError: Tensors must be contiguous" When re-running experiments
- Pull request#69yangky112024-08-29 21:28
- Pull request#70yangky112024-08-29 21:28
- Issue#68yangky112024-08-29 21:28RuntimeError: CUDA error: unspecified launch failure
Totals cover only the window loaded into ClickHouse and count events, not GitHub's lifetime totals — 200 stars here means stars gained during the window, not the repo's star count.