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.