Reproduce “crush: Extensible Proof Automation for Lean” on OpenResearch
Turn your favorite coding agents into research agents that review literature, develop hypotheses, and run experiments.
Universal app for Apple silicon and Intel. Requires macOS 11 or later.
About this paper
Mike He, Dexin Zhang, Aarti Gupta
crush translates Lean’s nondependent higher-order functions into first-order SMT representations using function sorts, application symbols, and equations for lambdas, then reconstructs solver results as proofs checked by Lean’s kernel. Across four suites totaling 754 verification conditions, it produced kernel-checked proofs for 693 (91.9%), versus 641 for grind. Its soundness result covers a monomorphic, nondependent fragment, not the full translation.
Summary by alphaXiv.
Tip: change arxiv.org to autoarxiv.org in any arXiv abstract link to open the paper here.