Kim Morrison - `grind`

Stream: Lean Together 2026

[Kim Morrison]

The slides for my talk at 2026-01-24T00:00:00+11:00 are available here:
grind @ Lean Together 2026.pdf

You can follow along the demo portions of my talk using the links to https://live.lean-lang.org/ embedded in the slides.

[Iván Renison]

I wanted to ask, how does grind compares with other types of proofs in efficiency? I have seen that in Mathlib some proofs are being replaced by grind, and I was wondering if that could slow down Mathlib building time?

[Jon Bannon]

Absolutely fantastic! Thank you for the exciting talk, Kim. I should probably check this first, but do the grind docs include any of the new capabilities, or is there a cheat sheet for the interactive mode yet? I guess, are there places beyond the walkthrough and your slides to learn about these new features? (I expect the answer is not yet...and the slides link nicely to sources, so I am not at all complaining!)

[Sébastien Boisgérault]

Great talk! :+1:

Beyond the slides (:pray: thanks!), is https://github.com/leanprover/lean4/blob/master/tests/lean/run/grind_guide.lean the best reference to learn more about the grind tactic?

[Kim Morrison]

The Lean Language Reference is the main source of documentation for grind:

https://lean-lang.org/doc/reference/latest/The--grind--tactic/#grind-tactic

[Kim Morrison]

Sébastien Boisgérault said:

Great talk! :+1:

Beyond the slides (:pray: thanks!), is https://github.com/leanprover/lean4/blob/master/tests/lean/run/grind_guide.lean the best reference to learn more about the grind tactic?

This is a good start, but this was written very early in the development of grind. It shows you how to do a lot of the basic stuff, but it is not complete for newer features.

[Mirek Olšák]

What would you think of a solver that handles integer equalities in a general commutative group? It could be practical for euclidean geometry (Real.angle). As far as I understand, grind doesn't handle it yet, and it can be solved efficiently & completely.
What exactly would I need to do if I want to add it?

[Kim Morrison]

In principle yes, however there have been enough revisions of the internal structure of grind that we haven't yet reached the point we have stable user extension points for solvers. It's still on our roadmap.

[Mirek Olšák]

Ok, then let me know when it is ready for users. Or add integer elimination directly... Here is a basic Lean implementation in 138 lines (without tracing proofs, and I do not guarantee it is bug-free).
IntElim.lean

[Ryan McCorvie]

Another person touched on this in the zoom chat, but I wanted to raise it here.

With "black box" tactics like grind and simp, there is no question of the soundness of any proof it generates. But from a software engineering perspective, couldn't changes in the tactic's implementation break proofs which used to work? I suppose this could happen if the implementation of any tactic changes, but it strikes me as more of a possibility with higher-level, more opaque tactics.

What mitigates this risk? Does software development tend to mostly only increase a tactic's scope of effectiveness rather than decrease it? Do these tactics have extensive test suites to check for breakage? Do the tactics themselves have proofs of their effectiveness in certain domains?

[Edward van de Meent]

there's a whole folder of tests, it seems...

[Chris Henson]

grind proofs do break occasionally. My anecdotal experience is that this is relatively limited. I've had it happen a few times, but often I felt it was my own fault for stretching what is reasonable for grind to infer and usually catch these in a nightly testing branch. It seems typical to leave an #adaptation_note in these situations, which you could search for if you're interested in observing stability over time.