Compfiles: Catalog Of Math Problems Formalized In Lean

Imo1976P5

module

public import Mathlib.Tactic

public section


/-!
# International Mathematical Olympiad 1976, Problem 5

n is a positive integer and m = 2n. aᵢⱼ = 0, 1 or -1 for 1 ≤ i ≤ n,
1 ≤ j ≤ m. The m unknowns x₁, x₂, ... , xₘ satisfy the n equations:

  aᵢ₁x₁ + aᵢ₂x₂ + ... + aᵢₘxₘ = 0,

for i = 1, 2, ... , n. Prove that the system has a solution in integers
of absolute value at most m, not all zero.
-/

namespace Imo1976P5

theorem imo1976_p5 (n : ℕ) (hn : 0 < n) (a : Fin n → Fin (2 * n) → ℤ)
    (ha : ∀ i j, a i j = 0 ∨ a i j = 1 ∨ a i j = -1) :
    ∃ x : Fin (2 * n) → ℤ,
      (∀ j, |x j| ≤ 2 * (n : ℤ)) ∧ (∃ j, x j ≠ 0) ∧
        ∀ i, ∑ j, a i j * x j = 0 := sorry

end Imo1976P5

File author(s): Kimi K3

This problem has a complete formalized solution.