NanoProof: Open and Efficient Automated Theorem Proving in Lean 4.

arXiv:2610.11605v1 Announce Type: cross Abstract: We introduce NanoProof, to our knowledge the first factorized execution-guided theorem prover in Lean 4 whose training data, extraction tooling, training pipeline, and weights are all released, making it end-to