Compfiles: Catalog Of Math Problems Formalized In Lean

Imo1971P6

import Mathlib.Data.Matrix.Basic
import Mathlib.Tactic

/-!
# International Mathematical Olympiad 1971, Problem 6

Let $A = (a_{ij})$ be an $n \times n$ matrix with non-negative integer entries.
Suppose that for all $i, j$, if $a_{ij} = 0$, then the sum of the elements in the
$i$-th row plus the sum of the elements in the $j$-th column is at least $n$.
Prove that the sum of all elements in the matrix is at least $n^2 / 2$.

-/

namespace Imo1971P6

theorem imo1971_p6 {n : ℕ} (A : Matrix (Fin n) (Fin n) ℕ) (n_pos : 0 < n)
    (h_cond : ∀ i j : Fin n, A i j = 0 → rowSum A i + colSum A j ≥ n) :
    2 * totalSum A ≥ n^2 := sorry

end Imo1971P6

File author(s): lean-tom (with assistance from Gemini)

This problem has a complete formalized solution.