An LLM with an REPL is a strong vericoding baseline in Lean

LLMs are rapidly changing how software is written. However, testing alone is insufficient; formal verification is therefore needed to rigorously guarantee correctness. Given a specification as the source of truth, LLMs can synthesize both the implementation and proof of conformance, a paradigm recently termed vericoding. These proofs are machine-checkable via interactive theorem provers such as Lean. While existing LLM-based provers demonstrate remarkable performance, they often constrain how LLMs interact with Lean. We ask how far we can push LLM performance without sophisticated harnesses by enabling direct interactive Lean usage. Our baseline, Tiny Prover, combines an iterative agent loop with direct interactive access to Lean. On VERINA and VeriSoftBench, we observe that this setup saturates both benchmarks, surpassing more complex prover architectures.