A new open-source Lean 4 theorem prover called NanoProof ships with everything: the data, the tooling, and the code, not just the weights.
NanoProof is a theorem-proving system built on a factorized execution-guided approach for the Lean 4 formal verifier. Its creators released the full pipeline alongside the model: a dataset of structured proof trees, a tool for extracting and interacting with Lean 4 programmatically, and the training code itself. On the MiniF2F-Test benchmark, it scores 50.8% pass@16, beating the two closest systems in its class, HyperTree Proof Search and ABEL, while using roughly 90 times and 7 times less compute respectively. It also trains on more than four orders of magnitude less compute than AlphaProof.
Most capable open-weight provers are fine-tuned on top of huge pretrained language models, and their makers release the weights but not the training data or pipeline. That leaves outsiders unable to verify how the system was built, let alone rebuild it. NanoProof's contribution is narrower: proof that this entire class of prover can be trained from scratch on modest hardware, and checked by anyone who wants to.
It's not the strongest theorem prover available - just the one you can actually audit end to end.