Mathematics in Lean

Stream: general

[Jeremy Avigad]

Patrick Massot and I have simplified and documented the procedures we use to produce Mathematics in Lean. Almost all of the content is written in Lean files which are then used to generate the textbook, the example files (which contain exercises), and the solutions. See the documentation in the source repository.

In a few places, the names MIL and mathematics_in_lean are hardcoded into the scripts, but the setup can be straightforwardly modified to write other Lean-based books as well. We'd be glad to answer questions for anyone who wants to try it.

[Jireh Loreaux]

Thanks very much for this documentation!

[Jeremy Avigad]

Mathematics in Lean (repository here) has been bumped to v4.20.0. It has a new chapter on formalizing discrete mathematics, and the last section of the previous chapter is also new.

Patrick and I are pleased that MIL has been holding up o.k., but it needs some care. We will make some updates and revisions this summer, address issues, introduce new tactics and automation, and so on.

[Cotasam Nemano]

Screenshot_20250720_081416.png
This is C03-S05, I completed the proof but the compiler said "failed to infer structural recursion", "well-founded recursion cannot be used". I am a newbie, so I don't understand why it is the case and how to fix it? Here is the code:

theorem lt_abs : x < |y| ↔ x < y ∨ x < -y := by
  constructor
  cases le_or_gt 0 y
  next h =>
    rw [abs_of_nonneg h]
    intro h; left; exact h
  next h =>
    rw [abs_of_neg h]
    intro h; right; exact h
  intro h₀
  cases h₀
  next h =>
    apply lt_abs.mpr
    left
    exact h
  next h =>
    apply lt_abs.mpr
    right
    exact h

[Cotasam Nemano]

Never mind. Thanks. I figured it out