Lean for Discrete mathematics proofs

Stream: lean4

[Anthony Chapov]

Hi everyone,

I am new to Lean and need help formalizing discrete math (intro) proofs. I use Lean as a part of my project, but I don't have much time to master the language. I would like to know what guides, libraries (with already formalized proofs) or parts of the Lean I need to use to be able to formalize very specific stuff like: sum of two odd is even; there is infinite amount of primes, product of odd is odd and so on..

Could someone help me with that?

[Chris Wong]

Welcome Anthony!

docs#Odd.odd_add
docs#Nat.exists_infinite_primes :smile:

To find these, I typed a bunch of relevant keywords in the search bar at the top. I've seen other people use "Loogle" or "Moogle" which are more sophisticated versions of this.

[Chris Wong]

(deleted)

[Chris Wong]

BTW, are you looking into discrete math in general, or only number theory? I think graphs, automata, and matroids all have significant gaps.

[Ruben Van de Velde]

Yet another approach is asking Lean itself:

import Mathlib

example {a b : Nat} (ha : Odd a) (hb : Odd b) : Even (a + b) := by exact?
-- Try this: exact Odd.add_odd ha hb

[Anthony Chapov]

Chris Wong писал/а:

BTW, are you looking into discrete math in general, or only number theory? I think graphs, automata, and matroids all have significant gaps.

Hey thank you for reply! I am working on translating informal proofs into formal proofs and look for proofs used in undergraduate discrete math courses. The ones that ask you to prove very basic stuff about primes, odds, evens, square roots of 2 is irrational, rational numbers and so on. I guess more like a properties of different numbers rather than Boolean algebra or graphs.

Because I try to translate the informal proofs (What student would write on paper) into formal proofs, I cant really use the simplified and implicit steps and need proofs in that form: theorem even_sum_even: ∀ x y, even x -> even y -> even (x + y) := by
intros x y h1 h2
unfold even at h1
unfold even at h2
cases h1 with
| intro k1 hk1 =>
cases h2 with
| intro k2 hk2 =>
exists (k1 + k2)
rw [hk1]
rw [hk2]
linarith

Instead of this (because the one below is not as explicit as the one above)

theorem Odd.add_odd : Odd m → Odd n → Even (m + n) := by
rintro ⟨m, rfl⟩ ⟨n, rfl⟩
refine' ⟨n + m + 1, _⟩
rw [two_mul, two_mul]
ac_rfl"