Compfiles: Catalog Of Math Problems Formalized In Lean

Imo1968P3

import Mathlib.Tactic

/-!
# International Mathematical Olympiad 1968, Problem 3

a, b, c are real with a non-zero. x1, x2, ... , xn satisfy the n equations:

        a x_i^2 + b x_i + c = x_{i+1}, for 1 ≤ i < n

        a x_n^2 + b x_n + c = x_1

Prove that the system has zero, 1 or >1 real solutions according as (b - 1)^2 - 4ac is <0, =0 or >0.
-/

namespace Imo1968P3

open Cardinal Finset

/- we define the solutionset as functions from ℕ to ℝ, that eventually vanish, as this allows summing over Finset.range
   as opposed to summing over Fin n -/

def solution_set (n : ℕ) (a b c : ℝ) : Set (ℕ → ℝ) := {x : ℕ → ℝ |
 (∀ i < n, a * (x i)^2 + b * (x i) + c = x (i+1)) ∧
 (a * (x n)^2 + b * (x n) + c = x 0) ∧ (∀ i > n, x i = 0)}

theorem imo1968_p3 {n : ℕ} (a b c : ℝ) (a_ne_zero : a ≠ 0) :
  (discrim a (b-1) c < 0 → #(solution_set n a b c) = 0) ∧
  (discrim a (b-1) c = 0 → #(solution_set n a b c) = 1) ∧
  (discrim a (b-1) c > 0 → #(solution_set n a b c) > 1) := sorry

end Imo1968P3

File author(s): John Maar

This problem has a complete formalized solution.