Another proof I just found (sorry, it's not about the formalization):
Let x be such that f(x) \neq 0 and let y \in \R. Set a = g(y).
Set u_n = f(x + ny) for n \in \Z. It satisfies the linear recurrence
relation u_{n+2} = 2a u_{n+1} - u_n. The characteristic relation is r^2 -
2ar + 1 = 0. The reduced discriminant is D = a^2 - 1. The sequence u_n is
bounded only if D \leq 0, that is, |a| \leq 1 (recall that f(x) \neq 0 and
the sequence is on \Z).
After inspection, it looks closer to Hales's solution. For formalization,
the other solution looks simpler since it does not use induction. The
least upper bound is defined in set.mm.
Benoît
On Thursday, February 27, 2020 at 6:08:41 PM UTC+1, Stanislas Polu wrote:
>
> Hi all,
>
> I'm quite a beginner with Metamath (I have read a bunch of proofs, most of
> the metamath book, I have implemented my own verifier, but I haven't
> constructed any original proof yet) and I am looking to formalize the
> following proof:
>
> IMO B2 1972: http://www.cs.ru.nl/~freek/demos/exercise/exercise.pdf
> Alternative version:
> http://www.cs.ru.nl/~freek/demos/exercise/exercise2.pdf
>
> (More broadly, I think this would be an interesting formalization to have
> in set.mm given this old but nonetheless interesting page:
> http://www.cs.ru.nl/~freek/demos/index.html)
>
> I am reaching out to the community to get direction on how should I go
> about creating an efficient curriculum for myself in order to achieve that
> goal? Any other advice is obviously welcome!
>
> Thank you!
>
> -stan
>
--
You received this message because you are subscribed to the Google Groups
"Metamath" group.
To unsubscribe from this group and stop receiving emails from it, send an email
to [email protected].
To view this discussion on the web visit
https://groups.google.com/d/msgid/metamath/27635ef7-bd62-4317-a0f2-9f0873e7c499%40googlegroups.com.
