How does Lean save on compute?

Stream: new members

[Tyler Josephson]

When I execute a proof that invokes high-level tactics (for example, the power operator) which are constructed from lower-level tactics (like multiplication, addition, succession, etc.), I have a feeling that the code isn't actually accessing or considering all of these lower tiers during runtime.

This makes it fast, right? How does this work? Is there a place I could read a bit more about it?

[Kevin Buzzard]

A tactic is something like induction or rw. Things like multiplication and addition are just regular functions, or terms. Lean is not actually doing any multiplications when you use the multiplication function -- it's meaningless to ask to compute "x * y" anyway, if x and y are random elements of a random ring. Lean's proof checking boils down to checking that a certain term has a certain type, rather than evaluating the term in any way.