Existence proofs

Stream: new members

[Michael Bucko]

Wrote those 2 proofs from The Mechanics of Proof. In both cases, I used use. Can I outsource the search to an ATP directly from Lean?

Proof 1

import Mathlib
import Lean

 example {p q : ℝ} (h : p < q) : ∃ x, p < x ∧ x < q := by
  use (p + q) / 2
  constructor
  · linarith
  · linarith

Proof 2

import Mathlib
import Lean

example (a : ℤ) : ∃ m n : ℤ, m ^ 2 - n ^ 2 = 2 * a + 1 := by
  use a+1
  use a
  linarith

Also, re-wrote the proof from the book like this:

It's a very interesting number

example : ∃ a b c d : ℕ,
    a ^ 3 + b ^ 3 = 1729 ∧ c ^ 3 + d ^ 3 = 1729 ∧ a ≠ c ∧ a ≠ d := by
  use 1, 12, 9, 10
  exact ⟨by norm_num, by norm_num, by norm_num, by norm_num⟩

[Bjørn Kjos-Hanssen]

At least this works (and is a sufficient search since 13^3 > 1729):

import Mathlib

example : ∃ a b c d : Fin (13),
    a ^ 3 + b ^ 3 = 1729 ∧ c ^ 3 + d ^ 3 = 1729 ∧ a ≠ c ∧ a ≠ d := by decide