LLMs and Lean: Making Proof Automation Practical for Dependent Types

We have proof automation now

I have long admired dependently-typed languages like Rocq and Lean for their ability to enforce complex invariants, but the massive time cost of manual proofs has kept them niche. Traditional automation tools like SMT solvers are often unpredictable and require deep expertise to manage. However, Large Language Models now offer a promising new path to automate proof generation, potentially making these powerful systems dramatically more practical for everyday engineering without the usual overhead.