Compfiles: Catalog Of Math Problems Formalized In Lean

Imo1975P6

import Mathlib

/-!
# International Mathematical Olympiad 1975, Problem 6

Find all polynomials P, in two variables, with the following properties:

(i) for a positive integer n and all real t, x, y
  P(tx, ty) = tⁿP(x, y)
(that is, P is homogeneous of degree n),

(ii) for all real a, b, c,
  P(b + c, a) + P(c + a, b) + P(a + b, c) = 0,

(iii) P(1, 0) = 1.
-/

namespace Imo1975P6

open Polynomial
open Polynomial.Bivariate

/- determine -/ abbrev solution_set : Set (ℝ[X][Y]) := sorry

theorem imo1975_p6 {P : ℝ[X][Y]} : P ∈ solution_set ↔
    (∃ n : ℕ+, ∀ t x y : ℝ, P.evalEval (t * x) (t * y) = t^n.val * P.evalEval x y)  ∧
    (∀ a b c : ℝ, P.evalEval (b+c) a + P.evalEval (c+a) b + P.evalEval (a+b) c = 0) ∧
    (P.evalEval 1 0 = 1) := sorry

end Imo1975P6

File author(s): Markus Rydh

This problem has a complete formalized solution.