Proof assistant demos at ICMS 2006

[ICMS 2006]

Exercise

Problem [B2 from IMO 1972]
f and g are real-valued functions defined on the real line. For all x and y,

f(x + y) + f(x - y) = 2 f(x) g(y).

f is not identically zero and |f(x)| ≤ 1 for all x. Prove that |g(x)| ≤ 1 for all x.

Solution
Let k be the least upper bound for |f(x)|. Suppose |g(y)| > 1. Then

2k ≥ |f(x + y)| + |f(x - y)| ≥ |f(x + y) + f(x - y)| = 2 |g(y)||f(x)|,

so |f(x)| ≤ k/|g(y)|. In other words, k/|g(y)| is an upper bound for |f(x)| which is less than k. Contradiction.

Demos

[demo session]
  1. Isabelle, try-out by Jeremy Avigad

    [Jeremy Avigad]
  2. HOL Light, demo by John Harrison

    [John Harrison]

    Video of the demo

  3. Mizar, demo by Artur Kornilowicz

    [Artur Kornilowicz]

    Video of the demo

  4. ProofPower, demo by Rob Arthan

    [Rob Arthan]

    Video of the demo

    • Polished version with both the demo proof and Hales' proof: pdf doc (doc does not mean "Word" here, but "ProofPower") (formalization times: about 77 minutes and about 35 minutes; de Bruijn factors: about 2.4 and about 2.0)
  5. Coq, demo by Laurent Théry

    [Laurent Théry]

    Video of the demo


(last modification 2006-09-21)