Minimum viable set of tactics for mathematics undergraduates

Stream: new members

[Isak Colboubrani]

For educational objectives, I aim to identify a "minimal viable set" of Lean and Mathlib tactics designed specifically for undergraduate mathematics students. This set is intended to strike a balance between being straightforward to avoid overwhelming learners, and being comprehensive enough to enable them to prove a broad spectrum of theorems encountered in undergraduate mathematics.

From an initial review of tactics covered across the following books I observe the following counts of unique tactics:

• Formalizing Mathematics ("FM"), covers 47 tactics
• Mathematics in Lean ("MIL"), covers 67 tactics
• The Hitchhiker’s Guide to Logical Verification ("HGLV"), covers 31 tactics

In other words:

|FM| = 47, |MIL| = 67, |HGLV| = 31

Combining these resources yields a total of 90 unique tactics, with an intersection of 13 tactics common across all texts:

|FM ∪ MIL ∪ HGLV| = 90
|FM ∩ MIL ∩ HGLV| = 13

Further analysis reveals intersections between pairs of texts:

|FM ∩ MIL| = 36
|FM ∩ HGLV| = 13
|MIL ∩ HGLV| = 19

Given these insights, the 13 tactics covered by all sources form a foundational "minimal set":

• apply
• assumption
• cases
• exact
• have
• induction
• intro
• linarith
• rfl
• ring
• rw
• show
• simp

This selection poses two key questions for further refinement:

1. Are there any "must have" tactics not included in this foundational set, considering the target audience of undergraduate mathematics students?
2. To optimize the balance between expressivity and simplicity, could any of these tactics be substituted with a more potent alternative that enhances expressivity without increasing the overall count of tactics?

[Damiano Testa]

aesop, refine, by_cases are missing and I think belong to your list!

[Damiano Testa]

by_contra is also something that corresponds directly to something that most students usually want to use. And constructor is very useful as well.

[Damiano Testa]

I personally also use rcases/obtain a lot and find convert often essential, especially for debugging or for quick-and-dirty proofs.

[Isak Colboubrani]

Thanks!

This is the "mention matrix" for the suggested tactics:

Tactic	FM	MIL	HGLV
aesop	✖	✖	:check:
by_cases	:check:	:check:	✖
by_contra	:check:	:check:	✖
constructor	:check:	:check:	✖
convert	:check:	:check:	✖
obtain	:check:	:check:	✖
rcases	:check:	:check:	✖
refine/refine'	:check:	:check:	✖

Key:

• FM: Formalizing Mathematics
• MIL: Mathematics in Lean
• HGLV: The Hitchhiker’s Guide to Logical Verification

[Patrick Massot]

The question is not specific enough. What kind of course do you want to run? Do you want to teach Lean or use Lean for teaching? What kind of mathematics do you want?

[Patrick Massot]

Looking at the tactics covered in the tutorial project is probably a better approximation.

[Jireh Loreaux]

For teaching, I don't see why you would want to exclude push_neg, contrapose and gcongr.

[Kevin Buzzard]

The list of tactics which I wrote my own documentation for, for the students in my class, is here. I should update it to include the tactics Jireh mentions; my main concern was getting documentation down which was more readable for mathematicians than the documentation supplied by Lean/mathlib.

[Patrick Massot]

Remember push_neg and contrapose were written as part of my teaching and later PRed to Mathlib.

[Patrick Massot]

The case of gcongr is a bit different. Depending on your goals you could argue it is too powerful. That's why rel also exists. Heather explicitly wrote it as a dumb version of gcongr intended for teaching very young students.

[Damiano Testa]

If you want some very anecdotal evidence, this is a tally of the tactics used in a random file from one of the projects that my students submitted:

      1 cases'
      1 constructor
      1 let
      1 nth_rw
      1 simp_rw
      2 choose
      2 induction'
      2 simp_all
      5 specialize
      6 unfold
     11 intro
     12 aesop
     13 apply
     18 simp
     49 rw
     61 exact
     90 have

[llllvvuu]

I use norm_num and decide a lot for stuff like (0 < 3) in Real. Maybe omega is worth mentioning too.

For specific domains, measurability, continuity, positivity, will probably be used a lot. Maybe with fun_prop merged some of the practice here will change (aesop-based versions seem to timeout a lot)

My noob cheese strategy is to spam have/suffices steps with exact?/apply?/simp?/simp_all?/aesop?/rw? and then go back and refactor/golf later.

[Miguel Marco]

I use cases' instead of cases (probably because a bias coming from Lean3).

I also use suffices, although you might probably get the same kind of functionality with have). And also calc can be very useful in some fields (but the user experience could be better, since you have to setup the skeleton with the steps first).

And definitely, use is a must if you want to prove existential statements.

In many proofs by induction I need to revert something first, to make sure that I have some hypothesis available adapted to the induction step.

And to prove disjunctions, left and right are a must for me.

[Ruben Van de Velde]

If you use revert with induction, you might find induction generalizing even more convenient