Proof assistant demos at ICMS 2006
Exercise
Problem [B2 from IMO 1972]
f and g are realvalued 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


Video of the demo

Video of the demo

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)

Video of the demo
(last modification 20060921)