CapSet

What is the minimum number $n$ such that for any set of $n$ integer triples $T$, there are three pair-wise distinct triples $(a_1, a_2, a_3), (b_1, b_2, b_3), (c_1, c_2, c_3) \in T$ with $a_1 + b_1 + c_1$, $a_2 + b_2 + c_2$, and $a_3 + b_3 + c_3$ all divisible by $3$.

Replace sorry in the template below with your solution. Mathlib version used by the checker is v4.31.0.

import Mathlib.Data.Finset.Card
import Mathlib.Order.Bounds.Defs

def answer : ℕ := sorry

def S : Set ℕ := { n | ∀ T : Finset (ℤ × ℤ × ℤ),
    T.card = n → ∃ a ∈ T , ∃ b ∈ T, ∃ c ∈ T, (a ≠ b ∧ b ≠ c ∧ c ≠ a) ∧
    (3 ∣ a.1 + b.1 + c.1) ∧ (3 ∣ a.2.1 + b.2.1 + c.2.1) ∧ (3 ∣ a.2.2 + b.2.2 + c.2.2) }

theorem solution : IsLeast S answer := sorry

Submit Solution

Login to submit a solution.

Recent Submissions