LeanGrowAlpha

LeanGrow is a work-in-progress tactic for proof-search, similar to Aesop, Canonical and Grind. It is currently not in a usable state. A short description of the approach it takes can be found in Report.pdf

Funding statement: This project is being funded by the Berlin Mathematics Research Center MATH+, itself funded by the German Research Foundation (DFG) under Germany’s Excellence Strategy (EXC-2046/1, project ID 390685689), and the Mathematical Research Data Initiative from January 2024 to December 2025.