LeanSketcher

LeanSketcher is a nascent Lean 4 project for automating inductive proofs and simplification. It provides lightweight custom tactics that combine structured induction, domain-specific simplification, and tactic backtracking to mimic "proof sketching."

This is a first step toward a broader system for proof sketch automation — blending user-supplied structure (e.g. "do induction") with tactical automation (e.g. try grind, split, simp, etc.).

The broader system would be a discovery system, integrating learning and LLMs.

Features

• auto_induction e: performs induction on e, followed by simplification using functions in the goal and grind/split strategies.
• auto_induction: automatically finds an inductive hypothesis to perform induction on.
• auto_simp: performs simp using all names that appear in the goal/hypotheses.

Repository structure

• LeanSketcher.lean: Main entry point for the tactics.
• LeanSketcher/Basic.lean: Internals -- so far, hardcoding auto_induction for the EvalOpt case study.
• LeanSketcher/Progress.lean: Automating a congruent case in a proof of progress.

Case studies

• EvalOpt.lean: demonstrates auto_induction tactic, even while the tactic is just a stub.
• StlcInd.lean: STLC with some manual proofs.
• SltcIndSketched.lean: demonstrates some automation over STLC proofs.

Inspirations

• Thanks to Arthur Adjedj for helping with the proofs that led to this automation.
• Study grind tactics. Examples in the test runs prefixed with grind_.
• Study the textbook for Interactive Theorem Proving at LMU SoSe 2025. This is the best resource I found for someone familiar with Rocq.
• Study Canonical for Automated Theorem Proving in Lean (paper, code).
• Study cmu-l3/llmlean for LLM integration from within Lean.
• Study Aesop for whitebox automation.
• Study lean-auto and Veil for SMT integration.