forwards maths and backwards lean proofs

Stream: new members

[rzeta0]

I am seeking advice from more experienced voices on this beginner question.

I've been exploring this Lean proof, which works fine.

import Mathlib.Tactic

lemma Nat.le_or_succ_le (a b : ℕ): a ≤ b ∨ b + 1 ≤ a := by
  rw [Nat.add_one_le_iff]
  exact le_or_lt a b

As part of that exploration I wanted to write down how I would prove such a lemma in plain maths, but still relying on the lemmas used in the lean proof.

---

Here is my simple sketch, assuming everything is a natural number:

• proof objective: $a \le b \lor b+1 \le a$
• known lemma: $n+1 \le m \iff n < m$ (lemma1)
• known lemma: $a\le b \lor b < a$ (lemma2)

then

• start with (lemma2) $a\le b \lor b < a$
• using (lemma1) we can say $(a\le b \lor b < a) \iff ( a\le b \lor b + 1 \le a)$
• the RHS matches our proof objective so we are done

---

My Question: The maths proof seems to run backwards to the Lean proof. Is this normal / common?

My Own Thoughts: Thinking about it, I suspect this happens often where the overall proof goal is transformed by tactics and hypotheses until it matches something known to be true, and thus resolved. Going in the "forward" direction would seem artificial in Lean where we start with have hypotheses based on Mathlib lemmas and build to wards the proof objective.

I'd welcome experienced voices on this, and whether I should be worried by my maths thinking going in the opposite direction of my Lean thinking.

[Scott Carnahan]

When I am stuck trying to formalize a math proof, I often write lots of haves and sorrys to set out what I know, and what steps I think might be fruitful. Sometimes, this yields a path to a solution. Then, I have a long, messy proof. After that, there is some cleaning up, where I delete unnecessary haves, split off lemmas that seem reasonably useful, and smoosh some parts together. During this process, sometimes switching the order of arguments can reduce the number of haves and makes the proof more in line with typical Lean flow.

When I am stuck in informal mathematics, my procedure is not so different. I don't think it should be a source of worry.