[tsimionescu]

I don't think you have any chance of approaching formal methods if the notation is a stumbling block.

The difficulty and verbosity of formal proofs is huge even with the very concise mathematical notation. And learning the notation itself is a very small stumbling block compared to learning the actual theorems and logic that you need to use.

So while I am not a fan of mathematical notation for general programming (which is often quite un-mathematical in fact) formal proofs are a place where this notation absolutely shines. I can't even imagine how much uglier the proof above would become if you had to replace `∀ (n : ℕ)` with something like `for any natural number n`.

[prisonguard]

there has to be a better way for a beginner to learn Lean even with the faintest high school mathematics recollection.

I can still do theorem proving in Idris excluding the mathematical notation and still learn concepts such as totality, covering, equality etc

[ykonstant]

A better way than what? The snippet you posted has nothing to do with how a beginner (or intermediate) learns Lean.

[sirwhinesalot]

Forall (n: Nat)

Is perfectly reasonable.

If conciseness was that important theorem provers would have syntax like APL.

[tsimionescu]

Why is forall any less formal than ∀? Or Nat less formal than ℕ? Especially when these are symbols that most will have learned in high school?

[sirwhinesalot]

They're not on my keyboard.