conditional forall

Stream: new members

[heather]

Hey yall, doing the lean4 tutorial and working on the exercises for chapter 4. just wondering how to write goldbach conjecture in a way that properly encodes it; I've written it as ∀ (x: Nat) (x_gt_2: x > 2) (x_even: even x), ∃ (a b: Nat), prime a ∧ prime b ∧ a + b = x and my editor tells me x_gt_2 and x_even are unused values, which indeed they are. is this correct? also, how would I write a meta-assertion that I've asserted goldbach's conjecture correctly, given that I don't intend to try my hand at proving or disproving the conjecture itself today?

[Alex J. Best]

What you have seens fine to me, except that you seem to have a mix of lean 3 and lean 4 style names. (i.e. Nat with a capital and even with a lowercase, did you define those yourself?)

You can write

def statement_of_goldbach : Prop :=  ∀ (x: Nat) (x_gt_2: x > 2) (x_even: even x), ∃ (a b: Nat), prime a ∧ prime b ∧ a + b = x

which just adds a specific named statement without any attempt at proof or disproof. The only meta-assertion here is that the name refers to the right thing. This may also complain about unused arguments but thats fine really

[heather]

even was from the tutorial, yes. https://leanprover.github.io/theorem_proving_in_lean4/quantifiers_and_equality.html#exercises - my solutions so far are:

def even (n : Nat) : Prop := ∃ k: Nat, 2 * k = n
def prime (n : Nat) : Prop := ¬ ∃ (j: Nat) (k: Nat), (0 < j) ∧ (j < n) ∧ (k < n) ∧ (k * j = n)
def infinitely_many_primes : Prop := ∀ a: Nat, ∃ b: Nat, b > a ∧ prime b
def Fermat_number (n : Nat) : Prop := ∃ k: Nat, (2^(2^k)) + 1 = n
def Fermat_prime (n : Nat) : Prop := Fermat_number n ∧ prime n
def infinitely_many_Fermat_primes : Prop := ∀ a: Nat, ∃ b: Nat, b > a ∧ Fermat_prime b
def goldbach_conjecture : Prop := ∀ (x: Nat) (x_gt_2: x > 2) (x_even: even x), ∃ (a b: Nat), prime a ∧ prime b ∧ a + b = x

copied literally from the tutorial, which uses these names exactly. I was just wondering, since I'm not sure of myself about syntax yet, whether there's any way to check definition correctness that is weaker than proof but stronger than just writing it down, like, idk, well I'm not sure what it'd be besides asking a human, to be honest, heh.

[Kevin Buzzard]

Interesting! That book was originally written in Lean 3, the conventions in Lean 4 now would be Even etc.

[Niels Voss]

The unused "values message" is just a warning. You can resolve it either by replacing (x_even : even x) with (_ : even x) or by using an implication like ∀ (x : Nat), x > 2 → even x → ∃ (a b: Nat), prime a ∧ prime b ∧ a + b = x.

There's generally no easy way to check to see if you have formalized a statement correctly (this is especially hard if you don't try to prove it). Sometimes you can use by slim_check to try to get Lean to generate counterexamples, but I think this won't work in this case because of the existential quantifier.