# Zulip Chat Archive

## Stream: new members

### Topic: conceptual mathematical primer for tactics?

#### Chris M (Jun 16 2020 at 04:10):

I haven't used tactics yet in Lean, and starting to. Looking at the tutorial, some of them seem unnatural to me, and it's not "clicking" yet for me. Can you point to a practice that mathematicians perform within informal mathematical proofs, to which tactics are analogous? Is it possible to say "tactics are the formal version of ...."?

#### Jalex Stark (Jun 16 2020 at 06:29):

tactics are programs that build proof terms

#### Jalex Stark (Jun 16 2020 at 06:29):

in informal math we don't build proof terms, we argue that we could build a proof term if we tried

#### Jalex Stark (Jun 16 2020 at 06:30):

`norm_num`

is a like a mathematician's `a short calculation shows...`

#### Utensil Song (Jun 16 2020 at 07:18):

I think it's a good idea to have such conceptual mathematical primer for tactics, I'll try to merge this idea into the cheat sheet idea here .

#### Matt Earnshaw (Jun 16 2020 at 15:52):

you may find it worthwhile to read at least the intro of Milner's paper that introduced the tactic idea, which gives a nice informal explanation https://royalsocietypublishing.org/doi/10.1098/rsta.1984.0067

If there are specific tactics that trouble you, feel free to ask about them. Some perhaps too obvious examples would be `apply`

as recognising that when `A -> B`

and we want to prove `B`

then it suffices to prove `A`

, and `intro`

as introducing an arbitrary `x : X`

when we want to prove a `forall x : X`

Last updated: May 13 2021 at 00:41 UTC