Trouble understanding the theorem process

Stream: lean4

[Phillip]

Hey, I am new to Lean/Lean4. I have a lot of software experience and am a math/comp sci student, but I am really struggling to comprehend the process of solving a proof.

I have been reading the docs in-and-out and attempting to solve something of my own.

open Nat

def divides (m n : Nat) : Prop := m % n = 0
notation m "|" n => divides n m

theorem evens_are_2n (m n : Nat) : (2|n) -> ∃m, n = 2*m :=
  sorry

Mathematically, I know this is a simple proof, having that, in general, you do a case by case proof, showing that only evens are in the form n=2*m. In this proof, I understand that there is the implication of being provided that n | 2, so all you'd need to do is show that there is an m that satisfies.

I am having trouble getting this into lean notation, and would very much appreciate it if someone can show me an example solution(s) and the process behind the reasoning for the code.

Thank you very much for your time!

[Johan Commelin]

@Phillip Usually we write $k \mid n$ for "$k$ divides $n$" (aka, $\exists c, n = k * c$, aka $n \% k = 0$)

[Johan Commelin]

Also, currently there is a lot more tutorials and learning material out there for Lean 3. We are currently preparing the transition to Lean 4, but this will take another X months before it is finished.

[Johan Commelin]

https://leanprover-community.github.io/learn.html

[Phillip]

Ahh! Thanks for that, silly typo

[Johan Commelin]

(Note that you can edit messages on Zulip, in case you want to fix the typo :wink: )

[Johan Commelin]

Concerning your particular proof. You'll want to provide a witness m. The obvious choice would be n / 2. And then you need to prove

n = 2 * (n / 2)

under the assumption n % 2 = 0.

[Johan Commelin]

That looks like something that you can prove by induction.

[Phillip]

Johan Commelin said:

Also, currently there is a lot more tutorials and learning material out there for Lean 3. We are currently preparing the transition to Lean 4, but this will take another X months before it is finished.

And yeah, I may end up doing that. I very much enjoy the lean4 syntax and thought that since I am only doing bare basics, by the time I am anywhere near proficient, it would release haha. But like you said, I may be better off doing lean 3 and those tutorials

[Johan Commelin]

I think that when you are starting out, the Lean 3 syntax and Lean 4 syntax are similar enough that it shouldn't matter for your first experiments.

[Phillip]

Johan Commelin said:

That looks like something that you can prove by induction.

I see, thanks! I will get looking into that (and lean 3 :laughing:)

[Phillip]

Johan Commelin said:

I think that when you are starting out, the Lean 3 syntax and Lean 4 syntax are similar enough that it shouldn't matter for your first experiments.

I will def go back and give it a good look. Thank you :)

[Kevin Buzzard]

Is it me or is this theorem false? It seems to me that the original question is asking to prove that if n=1 or n=2 then n is even, which is false

[Kevin Buzzard]

Note that divides x y would be pronounced "y divides x" by a mathematician

[Phillip]

Kevin Buzzard said:

Is it me or is this theorem false? It seems to me that the original question is asking to prove that if n=1 or n=2 then n is even, which is false

Yeah, I messed up the definition. Probably another reason I have had issues with getting it proven haha

[Kevin Buzzard]

I don't think you did mess up the definition, this is my point

[Kevin Buzzard]

I think you messed up the theorem

[Kevin Buzzard]

Oh ok you changed it