A short introduction to the grind tactic

 A short introduction to the grind tactic🔗

Hannah Scholz

This is the write-up for the talk about the grind tactic for the Graduate Seminar "Advanced Topics in Formalised Mathematics" taught by Michael Rothgang in Bonn in the summer term 2026. This document is mostly based on the Lean Language Reference, so look there for further reading.

grind is still a relatively new tactic. It was announced in July 2025 (see the Zulip announcement here) and is still in active development. So this document might already be out of date in the near future. It was written July 2026.

Contents

  1. 1. Basic usage of grind
  2. 2. Intuition of how grind works
  3. 3. Understanding error messages
  4. 4. Basic derivations of new facts
  5. 5. E-matching
  6. 6. Satellite solvers
  7. 7. Interactive mode
  8. 8. Miscellaneous further things
  9. 9. Sources and Resources