How would I go about learning to translate basic proofs?

Stream: lean4

[Sabbir Rahman]

My motivation for lean (for now) is to translate easy proofs that I know to lean. For example consider this, the sum of natural numbers from 0 to n is n*(n+1)/2. I am well aware of how to prove this rigorously. But how will I do it in lean? Or even more basic how would I translate this statement to lean? I looked through theorem proving in lean partially and I do get how to use tactics for simple propositional logic. But could someone guide me how to go about doing the example I gave, so that in the process I understand how to do many more proofs like it?

[Kevin Buzzard]

Here's the statement:

import tactic

open_locale big_operators

open finset

example (n : ℕ) : ∑ i in range n, (i : ℚ) = n * (n - 1) / 2 :=
begin
  sorry
end

It's n-1 not n+1 becaue range n is [0...(n-1)]. You'll not find much maths in Theorem Proving in Lean, you want to look at a more mathsy thing like Mathematics in Lean or the course I'm currently teaching.

[Henrik Böving]

(note that the syntax used by Kevin is Lean 3 + mathlib, not Lean 4)

[Kevin Buzzard]

Oh apologies, I hadn't noticed the stream! All my suggestions are also Lean 3. I'm afraid there's very little publically available teaching material for mathlib + lean 4 right now. @Heather Macbeth do you have anything public?

[Heather Macbeth]

Yup, here's that example in my lecture notes!
https://hrmacbeth.github.io/math2001/06_Induction.html#id11

[Heather Macbeth]

I don't cover finsets though.

[Kevin Buzzard]

The Finset version in lean 4 is

import Mathlib.Algebra.BigOperators.Basic
import Mathlib.Data.Rat.Basic

open BigOperators Finset

example (n : ℕ) : ∑ i in range n, (i : ℚ) = n * (n - 1) / 2 := by
  sorry

but you might be better off following a coherent course rather than just trying to solve random problems (says the person who learnt Lean by just solving random problems and then asking here when he got stuck)

[Heather Macbeth]

@Sabbir Rahman, my lecture notes are designed for students who don't yet know how to do these "easy proofs" on paper, so I deliberately work in a somewhat special Lean dialect, using only a small subset of the tactics+theory available in mathlib. There is still coverage of all the "easy proofs" in a standard course (or there will be when the semester finishes), but the approach is not always the conventional-in-mathlib approach.

[Sabbir Rahman]

Heather Macbeth said:

Sabbir Rahman, my lecture notes are designed for students who don't yet know how to do these "easy proofs" on paper, so I deliberately work in a somewhat special Lean dialect, using only a small subset of the tactics+theory available in mathlib. There is still coverage of all the "easy proofs" in a standard course (or there will be when the semester finishes), but the approach is not always the conventional-in-mathlib approach.

Your notes seem very helpful, I'll try to follow them to familiarize with basic techniques. But I still have the question of how would I learn about new concepts? For example, here I needed big operators. How would I have learnt that summation translates to a big operator. Or perhaps one day I tried to prove something about probability distributions, how would I learn what the proper translation blocks are?

[Kevin Buzzard]

Right now you either ask in #new members or you read teaching materials -- this is how you learn anything, right?