Searching for Proof Improvements with tryAtEachStep

Abstract: I will present tryAtEachStep, a tool that walks through Lean source code and runs a given tactic on every proof step. I will discuss how it is implemented, a variety of different ways it might be used, and some results from running it on Mathlib.

logic in computer sciencemathematical softwareMathematics

Audience: researchers in the discipline

( video )

Lean Together 2025

Series comments: Most of the talks from the conference are available on YouTube: www.youtube.com/watch?v=ZPPDktjL1Lw&list=PLlF-CfQhukNlzXdQvu1SVt9vcD4--fLlg