AI-MO/CombiBench huggingface dataset:
Problem: How many ways can a teacher select a group of 6 students to sit in the front row if the class has 13 students?
Answer: 1716

Lean formal statement:
import Mathlib

theorem hackmath_1 (sols : Finset (Fin 13 → Fin 2))
    (h_sols : ∀ f, f ∈ sols ↔ ((List.ofFn f).count 0 = 6)) :
    sols.card = ((1716) : ℕ ) := by sorry
Problem: There are 8 athletes participating in a sprint competition. The referee needs to select 3 athletes and assign them specific rankings (first place, second place, and third place). How many different arrangements are possible?
Answer: 336

Lean formal statement:
import Mathlib

theorem hackmath_2 (sols : Finset (Fin 8 → Fin 4))
    (h_sols : ∀ f, f ∈ sols ↔
      ((List.ofFn f).count 0 = 1) ∧ ((List.ofFn f).count 1 = 1) ∧ ((List.ofFn f).count 2 = 1)) :
    sols.card = ((336) : ℕ ) := by sorry
Problem: How many four-digit numbers can be formed from the numbers 3 5 8 9 if they are not allowed to be repeated?
Answer: 24

Lean formal statement:
import Mathlib

theorem hackmath_3 (sol : Finset ℕ)
    (h_sol : ∀ s, s ∈ sol ↔ 1000 ≤ s ∧ s ≤ 9999 ∧ (Nat.digits 10 s).toFinset = {3, 5, 8, 9}) :
    sol.card = ((24) : ℕ ) := by sorry
Problem: How many people must be in a group for at least two of them to be born in the same month?
Answer: 13

Lean formal statement:
import Mathlib

theorem hackmath_4 : IsLeast {n | ∀ f : Fin n → Fin 12, ∃ a b, f a = f b} ((13) : ℕ ) := by sorry
Problem: There are 10 red marbles, 6 green marbles, and 4 blue marbles in a box. What is the probability of picking the next red marble?
Answer: 1 / 2

Lean formal statement:
import Mathlib

open MeasureTheory ProbabilityTheory ENNReal

theorem hackmath_5 : uniformOn (Ω := (Fin 20)) ⊤ {i | i.1 < 10} = ((1 / 2) : ENNReal ) := by sorry
Problem: Two coins are tossed simultaneously. What is the probability of getting (i) At least one head? (ii) At most one tail? (iii) A head and a tail?
Answer: 3 / 4, 3 / 4, 1 / 2

Lean formal statement:
import Mathlib

theorem hackmath_6 : PMF.binomial (1/2 : _) ENNReal.half_le_self 2 1 +
    PMF.binomial (1/2 : _) ENNReal.half_le_self 2 2 = ((3 / 4) : ENNReal ) ∧
    PMF.binomial (1/2 : _) ENNReal.half_le_self 2 0 +
    PMF.binomial (1/2 : _) ENNReal.half_le_self 2 1 = ((3 / 4) : ENNReal ) ∧
    PMF.binomial (1/2 : _) ENNReal.half_le_self 2 1 = ((1 / 2) : ENNReal ) := by sorry
Problem: The group of 10 girls should be divided into two groups with at least four girls in each group. How many ways can this be done?
Answer: 462

Lean formal statement:
import Mathlib

theorem hackmath_7 (sols : Finset (Finpartition (@Finset.univ (Fin 10))))
    (h_sols : ∀ f, f ∈ sols ↔ (f.parts.card = 2) ∧ (∀ i, i ∈ f.parts → i.card ≥ 4)) :
    sols.card = ((462) : ℕ ) := by sorry
Problem: A ferry with a capacity of 10 people takes a group of 13 men and 7 women across a river. Find the number of ways in which the group may be taken across the if all women go on the first group.
Answer: 286

Lean formal statement:
import Mathlib

theorem hackmath_8 (sols : Finset ((Fin 13 → Fin 2) × (Fin 7 → Fin 2)))
    (h_sols : ∀ f, f ∈ sols ↔ (∀ i, f.2 i = 0) ∧ ∀ k, ((List.ofFn f.1).count k  + (List.ofFn f.2).count k = 10)) :
    sols.card = ((286) : ℕ ) := by sorry
Problem: The father has six sons and ten identical, indistinguishable balls. How many ways can he give the balls to his sons if everyone gets at least one?
Answer: 126

Lean formal statement:
import Mathlib

theorem hackmath_9 (sols : Finset (Fin 6 → ℕ))
    (h_sols : ∀ f, f ∈ sols ↔ ((∀ i, f i > 0) ∧ (∑ i, f i = 10))) :
    sols.card = ((126) : ℕ ) := by sorry
Problem: How many different ways can three people divide seven pears and five apples?
Answer: 756

Lean formal statement:
import Mathlib

theorem hackmath_10 (sols : Finset (Fin 3 → (ℕ × ℕ)))
    (h_sols : ∀ f, f ∈ sols ↔ (∑ i, (f i).1 = 7 ∧ ∑ i, (f i).2 = 5)) :
    sols.card = ((756) : ℕ ) := by sorry
Problem: Show that the result of replacing every integer a in a magic square of order n with $n^2 + 1 − a$ is a magic square of order n.

Lean formal statement:
import Mathlib

structure IsMagicSquare {n : ℕ} (M : Matrix (Fin n) (Fin n) ℕ) : Prop where
  mem : ∀ i j, M i j ∈ Finset.Icc 1 (n * n)
  pairwise : ∀ i j i' j', i ≠ i' ∨ j ≠ j' → M i j ≠ M i' j'
  same_sum : ∃ s, (∀ i, ∑ j, M i j = s) ∧ (∀ j, ∑ i, M i j = s) ∧ (∑ i, M i i.rev = s) ∧ ∑ i, M i i = s

abbrev replace {n : ℕ}: Matrix (Fin n) (Fin n) ℕ → Matrix (Fin n) (Fin n) ℕ :=
  fun A i j ↦ n^2 + 1 - A i j

theorem brualdi_ch1_16 {n : ℕ} (M : Matrix (Fin n) (Fin n) ℕ) (hM : IsMagicSquare M) :
    IsMagicSquare (replace M) := by sorry
Problem: Verify that there is no magic square of order 2.

Lean formal statement:
import Mathlib

structure IsMagicSquare {n : ℕ} (M : Matrix (Fin n) (Fin n) ℕ) : Prop where
  mem : ∀ i j, M i j ∈ Finset.Icc 1 (n * n)
  pairwise : ∀ i j i' j', i ≠ i' ∨ j ≠ j' → M i j ≠ M i' j'
  same_sum : ∃ s, (∀ i, ∑ j, M i j = s) ∧ (∀ j, ∑ i, M i j = s) ∧ (∑ i, M i i.rev = s) ∧ ∑ i, M i i = s

theorem brualdi_ch1_10 : ¬∃ (M : Matrix (Fin 2) (Fin 2) ℕ), IsMagicSquare M := by sorry
Problem: Find the number of different perfect covers of a 3-by-4 chessboard by dominoes.
Answer: 9

Lean formal statement:
import Mathlib

structure Domino (n k : ℕ) where
  carrier : Finset (Fin n × Fin (2 * k))
  card : carrier.card = 2
  
  position : ∀ i ∈ carrier, ∀ j ∈ carrier, i ≠ j →
    
    (i.1.val = j.1.val ∧ (i.2.val + 1 = j.2.val ∨ j.2.val + 1 = i.2.val)) ∨ 
    
    (i.2.val = j.2.val ∧ (i.1.val + 1 = j.1.val ∨ j.1.val + 1 = i.1.val))

noncomputable instance {n k} : Fintype (Domino n k) :=
  Fintype.ofInjective Domino.carrier <| by
    rintro ⟨carrier, _⟩ ⟨carrier', _⟩ (rfl : carrier = carrier')
    rfl

structure PerfectCover (n k : ℕ) where
  
  d_set : Finset (Domino n k)
  d_card : d_set.card = n * k
  
  covers : ∀ i : Fin n × Fin (2 * k), ∃ d ∈ d_set, i ∈ d.carrier

noncomputable instance {n k} : Fintype (PerfectCover n k) :=
  Fintype.ofInjective PerfectCover.d_set <| by
    rintro ⟨d, _⟩ ⟨d', _⟩ (rfl : d = d')
    rfl

theorem brualdi_ch1_5 : Fintype.card (PerfectCover 3 2) = ((9) : ℕ ) := by sorry
Problem: How many integers greater than 5400 have both of the following properties? (a) The digits are distinct. (b) The digits 2 and 7 do not occur.
Answer: 94830

Lean formal statement:
import Mathlib

theorem brualdi_ch2_6 (s : Finset ℕ)
    (hs : ∀ n, n ∈ s ↔ n > 5400 ∧ (Nat.digits 10 n).Nodup ∧ 2 ∉ (Nat.digits 10 n) ∧ 7 ∉ (Nat.digits 10 n)) :
    s.card = ((94830) : ℕ ) := by sorry
Problem: Determine the total number of combinations (of any size) of a multiset of objects of $k$ different types with finite repetition numbers $n_{1}, n_{2}, \ldots, n_{k}$, respectively.
Answer: fun n => (∑ i : Fin k, (n i + 1))

Lean formal statement:
import Mathlib

theorem brualdi_ch2_36 {k : ℕ} (n : Fin k → ℕ)
    (sols : Finset (Fin k → ℕ))
    (h_sols : ∀ f, f ∈ sols ↔ (∀ i, f i ≤ n i)) :
    sols.card = ((fun n => (∑ i : Fin k, (n i + 1))) : (Fin k → ℕ) → ℕ ) n := by sorry
Problem: How many sets of three integers between 1 and 20 are possible if no two consecutive integers are to be in a set?
Answer: 816

Lean formal statement:
import Mathlib

open Finset

theorem brualdi_ch2_11 :
    ((Icc (1 : ℕ) 20).powersetCard 3 |>.filter (fun S => ∀ a ∈ S, a - 1 ∉ S ∧ a + 1 ∉ S)).card =
    ((816) : ℕ ) := by sorry
Problem: Prove that of any five points chosen within a square of side length 2 , there are two whose distance apart is at most $\sqrt{2}$.

Lean formal statement:
import Mathlib

theorem brualdi_ch3_18
    (points : Fin 5 → (EuclideanSpace ℝ (Fin 2)))
    (h_points : ∀ i, 0 ≤ ((points i) 0) ∧ ((points i) 0) ≤ 2 ∧ 0 ≤ ((points i) 1) ∧ ((points i) 1) ≤ 2) :
    ∃ i j, i ≠ j ∧ dist (points i) (points j) ≤ √2 := by sorry
Problem: Show that if $n+1$ integers are chosen from the set ${1,2, \ldots, 2 n}$, then there are always two which differ by 1.

Lean formal statement:
import Mathlib

theorem brualdi_ch3_4 (n : ℕ) (S : Finset ℕ) (elem_range : ∀ s ∈ S, (1 ≤ s ∧ s ≤ 2 * n))
    (card : S.card = n + 1) : ∃ s ∈ S, ∃ s' ∈ S, s = s' + 1 := by sorry
Problem: A collection of subsets of ${1,2, \ldots, n}$ has the property that each pair of subsets has at least one element in common. Prove that there are at most $2^{n-1}$ subsets in the collection.

Lean formal statement:
import Mathlib

theorem brualdi_ch3_27 (n : ℕ) (hn : n ≥ 1)
    (subsets : Set (Set (Set.Icc 1 n)))
    (cond : ∀ S ∈ subsets, ∀ T ∈ subsets, (S ∩ T).Nonempty) :
    ∃ (m : ℕ), m ≤ 2 ^ (n - 1) ∧ Nonempty (Fin m ≃ subsets) := by sorry
Problem: The complement $\bar{A}$ of an $r$-subset $A$ of $\{1,2, \ldots, n\}$ is the $(n-r)$-subset of $\{1,2, \ldots, n\}$, consisting of all those elements that do not belong to $A$. Let $M=\binom{n}{r}$, the number of $r$-subsets and, at the same time, the number of $(n-r)$ subsets of $\{1,2, \ldots, n\}$. Prove that, if $A_{1}, A_{2}, A_{3}, \ldots, A_{M}$ are the $r$-subsets in lexicographic order, then $\overline{A_{M}}, \ldots, \overline{A_{3}}, \overline{A_{2}}, \overline{A_{1}}$ are the $(n-r)$-subsets in lexicographic order.

Lean formal statement:
import Mathlib

open List Lex

theorem brualdi_ch4_35 (r n M : ℕ) (hM : M = ((@Finset.univ (Fin n)).powersetCard r).card)
    (A : Fin M → (Finset.powersetCard r (@Finset.univ (Fin M) _))) :
    ∀ i j, (List.Lex (fun x1 x2 : Fin M => x1 ≤ x2)
    (Finset.sort (· ≤ ·) (A i)) (Finset.sort (· ≤ ·) (A j))) →
    (List.Lex (fun x1 x2 : Fin M => x1 ≤ x2)
    (Finset.sort (· ≤ ·) (A j)ᶜ) (Finset.sort (· ≤ ·) (A i)ᶜ)) := by sorry
Problem: Let $n \geq 2$ be an integer. Prove that the total number of inversions of all $n$ ! permutations of $1,2, \ldots, n$ equals $\frac{1}{2} n!\binom{n}{2}=n!\frac{n(n-1)}{4}$ (Hint: Pair up the permutations so that the number of inversions in each pair is $\frac{n(n-1)}{2}$.)

Lean formal statement:
import Mathlib

def invNum {n : ℕ} (σ : Equiv.Perm (Fin n)) : ℕ :=
  ∑ x ∈ Equiv.Perm.finPairsLT n, if σ x.fst ≤ σ x.snd then 1 else 0

theorem brualdi_ch4_59 (n : ℕ) (hn : n ≥ 2) : ∑ σ : Equiv.Perm (Fin n), invNum σ =
    n.factorial * n * (n - 1) / 4 := by sorry
Problem: Show that the largest number of inversions of a permutation of ${1, 2, ... , n}$ equals $\frac{n(n -1)}{2}$.

Lean formal statement:
import Mathlib

def invNum {n : ℕ} (σ : Equiv.Perm (Fin n)) : ℕ :=
  ∑ x ∈ Equiv.Perm.finPairsLT n, if σ x.fst ≤ σ x.snd then 1 else 0

theorem brualdi_ch4_9 (n : ℕ) :
    IsGreatest {k | ∃ σ : Equiv.Perm (Fin n), k = invNum σ} (n * (n - 1) / 2) := by sorry
Problem: Let $R$ and $S$ be two partial orders on the same set $X$. Considering $R$ and $S$ as subsets of $X \times X$, we assume that $R \subseteq S$ but $R \neq S$. Show that there exists an ordered pair $(p, q)$, where $(p, q) \in S$ and $(p, q) \notin R$ such that $R^{\prime}=R \cup\{(p, q)\}$ is also a partial order on $X$.

Lean formal statement:
import Mathlib

theorem brualdi_ch5_51 {X : Type} [DecidableEq X] (R S : Rel X X) [IsPartialOrder X R]
    [IsPartialOrder X S] (le : R < S) :
    ∃ (p q : X), S p q ∧ ¬ R p q ∧
    IsPartialOrder X (R ⊔ fun x y ↦ if x = p ∧ y = q then true else false) := by sorry
Problem: Evaluate the sum $\sum_{k=0}^{n}(-1)^{k}\binom{n}{k} 10^{k}$.
Answer: fun n => (-9 : ℤ)^n

Lean formal statement:
import Mathlib

theorem brualdi_ch5_9 (n : ℕ) : ∑ k ∈ Finset.range (n + 1), (-1 : ℤ) ^ k * (n.choose k) * 10 ^ k =
    ((fun n => (-9 : ℤ)^n) : ℕ → ℤ ) n := by sorry
Problem: Let $n$ and $k$ be integers with $1 \leq k \leq n$. Prove that $\sum_{k=1}^{n}\binom{n}{k}\binom{n}{k-1}=\frac{1}{2}\binom{2 n+1}{n+1}-\binom{2 n}{n}$.

Lean formal statement:
import Mathlib

theorem brualdi_ch5_26 (n k : ℕ) (h1 : 1 ≤ k) (h2 : k ≤ n) :
    ∑ k ∈ Finset.Icc 1 n, Nat.choose n k * Nat.choose n (k - 1) =
    (1 / 2 : ℚ) * Nat.choose (2 * n + 1) (n + 1) - Nat.choose (2 * n) n := by sorry
Problem: Determine the number of permutations of $\{1,2, \ldots, 8\}$ in which no even integer is in its natural position.
Answer: 24024

Lean formal statement:
import Mathlib

theorem brualdi_ch6_11
    (sols : Finset (Equiv.Perm (Finset.Icc 1 8)))
    (h_sols : ∀ σ, σ ∈ sols ↔ (∀ i, Even i.1 → σ i ≠ i)) :
    sols.card = ((24024) : ℕ ) := by sorry
Problem: Prove that $D_{n}$ is an even number if and only if $n$ is an odd number.

Lean formal statement:
import Mathlib

theorem brualdi_ch6_21 (n : ℕ) : Even (numDerangements n) ↔ Odd n := by sorry
Problem: Determine the number of integral solutions of the equation $x_{1}+x_{2}+x_{3}+x_{4}=20$ that satisfy $1 \leq x_{1} \leq 6,0 \leq x_{2} \leq 7,4 \leq x_{3} \leq 8,2 \leq x_{4} \leq 6$.
Answer: 96

Lean formal statement:
import Mathlib

open Finset

theorem brualdi_ch6_9 : {x : Fin 4 → ℕ | ∑ i, x i = 20 ∧ x 0 ∈ Icc 1 6 ∧ x 1 ∈ Icc 0 7 ∧
    x 2 ∈ Icc 4 8 ∧ x 3 ∈ Icc 2 6}.ncard = ((96) : ℕ ) := by sorry
Problem: Determine the generating function for the sequence of cubes \[ 0, 1, 8, \ldots, n^{3}, \ldots \]
Answer: PowerSeries.X * (PowerSeries.X ^ 2 + 4 * PowerSeries.X + 1) * PowerSeries.inv (1 - PowerSeries.X) ^ 4

Lean formal statement:
import Mathlib

theorem brualdi_ch7_15 : PowerSeries.mk (fun (n : ℕ) => (n : ℝ) ^ 3) = ((PowerSeries.X * (PowerSeries.X ^ 2 + 4 * PowerSeries.X + 1) * PowerSeries.inv (1 - PowerSeries.X) ^ 4) : PowerSeries ℝ ) := by
    sorry
Problem: Let $m$ and $n$ be positive integers whose greatest common divisor is $d$. Prove that the greatest common divisor of the Fibonacci numbers $f_{m}$ and $f_{n}$ is the Fibonacci number $f_{d}$.

Lean formal statement:
import Mathlib

theorem brualdi_ch7_7 (m n d : ℕ+) (hmd : d = Nat.gcd m n) :
    Nat.gcd (Nat.fib m) (Nat.fib n) = Nat.fib d := by sorry
Problem: Determine the number of n-digit numbers with all digits odd, such that 1 and 3 each occur a nonzero, even number of times.
Answer: fun n => (5 ^ n - 4 ^ (n + 1) + 6 * 3 ^ n - 4 * 2 ^ n + 1) / 4 

Lean formal statement:
import Mathlib

abbrev S (n : ℕ) : Finset ℕ :=
  {m < 10^n | (Nat.digits 10 m).length = n ∧
  (∀ i : Fin (Nat.digits 10 m).length, Odd ((Nat.digits 10 m).get i)) ∧
  Even ((Nat.digits 10 m).count 1) ∧ Even ((Nat.digits 10 m).count 3) ∧
  ((Nat.digits 10 m).count 1) ≠ 0 ∧ ((Nat.digits 10 m).count 3) ≠ 0}

theorem brualdi_ch7_27 (n : ℕ) : (S n).card = ((fun n => (5 ^ n - 4 ^ (n + 1) + 6 * 3 ^ n - 4 * 2 ^ n + 1) / 4 ) : ℕ → ℕ ) n := by sorry
Problem: Let the sequence $h_{0}, h_{1}, \ldots, h_{n}, \ldots$ be defined by $h_{n}=2 n^{2}-n+3,(n \geq 0)$. Find a formula for $\sum_{k=0}^{n} h_{k}$.
Answer: fun n => ((n + 1) * (4 * n ^ 2 - n + 18) / 6)

Lean formal statement:
import Mathlib

theorem brualdi_ch8_6 (n : ℕ) (h : ℕ → ℝ) (h' : ∀ i, h i = 2 * i ^ 2 - i + 3) :
    ∑ i ∈ Finset.range (n + 1), h i = ((fun n => ((n + 1) * (4 * n ^ 2 - n + 18) / 6)) : ℕ → ℝ ) n := by sorry
Problem: Prove that the partition function satisfies $p_{n} > p_{n-1}$ when $2 ≤ n$.

Lean formal statement:
import Mathlib

theorem brualdi_ch8_30 (n : ℕ) (hn : 2 ≤ n) :
    Fintype.card (Nat.Partition (n - 1)) < Fintype.card (Nat.Partition n) := by sorry
Problem: Prove that the following formula holds for the $k$ th-order differences of a sequence $h_{0}, h_{1}, \ldots, h_{n}, \ldots$ : \Delta^{k} h_{n}=\sum_{j=0}^{k}(-1)^{k-j}\binom{k}{j} h_{n+j}

Lean formal statement:
import Mathlib

theorem brualdi_ch8_9 (h : ℕ → ℤ) (k n : ℕ): (fwdDiff 1)^[k] h n = ∑ j ∈ Finset.range (k + 1),
    (-1 : ℤ) ^ (k - j) * Nat.choose k j * h (n + j) := by sorry
Problem: Let $A$ be a matrix with $n$ columns, with integer entries taken from the set $S=\{1,2, \ldots, k\}$. Assume that each integer $i$ in $S$ occurs exactly $n r_{i}$ times in $A$, where $r_{i}$ is an integer. Prove that it is possible to permute the entries in each row of $A$ to obtain a matrix $B$ in which each integer $i$ in $S$ appears $r_{i}$ times in each column.

Lean formal statement:
import Mathlib

theorem brualdi_ch9_13 (n m k : ℕ) (r : ℕ → ℕ) (A : Matrix (Fin m) (Fin n) ℕ)
    (hn : n > 0) (hm : m > 0)(hk : k ≥ 1)
    (hA : ∀ i j, A i j ∈ Finset.Icc 1 k)
    (hr : ∀ i ∈ Finset.Icc 1 k, (∑ x : Fin m, ∑ y : Fin n, if A x y = i then 1 else 0) = n * r i) :
    ∃ (rσ : Fin m → Equiv.Perm (Fin n)),
      ∀ j : Fin n, ∀ i ∈ Finset.Icc 1 k,
      (∑ x : Fin m, if A x ((rσ x) j) = i then 1 else 0) = r i := by sorry
Problem: Let $\mathcal{A}=\left(A_{1}, A_{2}, A_{3}, A_{4}, A_{5}, A_{6}\right)$, where \[ \begin{aligned} & A_{1}=\{1,2\}, A_{2}=\{2,3\}, A_{3}=\{3,4\} \\ & A_{4}=\{4,5\}, A_{5}=\{5,6\}, A_{6}=\{6,1\} \end{aligned} \] Determine the number of different SDRs that $\mathcal{A}$ has.
Answer: 2

Lean formal statement:
import Mathlib

variable {α : Type*}

structure SDR {n : ℕ} (A : Fin n → Finset α) where
  toFun : Fin n → α
  mem_Ai : ∀ i, toFun i ∈ A i
  pairwise : ∀ i j, i ≠ j → toFun i ≠ toFun j

instance {n : ℕ} (A : Fin n → Finset α) : CoeFun (SDR A) (fun _ => Fin n → α) where
  coe s := s.toFun

noncomputable instance {n : ℕ} (A : Fin n → Finset α) : Fintype (SDR A) := by
  classical
  let Y := Finset.biUnion (@Finset.univ (Fin n) _) A
  if h : Nonempty (SDR A) then
    exact Fintype.ofSurjective (α := (Fin n → Y))
      (fun f ↦ if h1 : (∃(g : SDR A), ∀ i, f i = g i) then ⟨fun i => f i,
          fun i ↦ by have ⟨g, hg⟩ := h1; simp [hg, g.mem_Ai],
          fun i j hij ↦ by have ⟨g, hg⟩ := h1; simp [hg, g.pairwise i j hij]⟩
        else Classical.choice (α := (SDR A)) h) <| fun g ↦
          ⟨fun i => ⟨g i, by simp [Y]; use i; simp [g.mem_Ai]⟩, by
            simp; suffices ∃ (g' : SDR A), ∀ (i : Fin n), g.toFun i = g'.toFun i by simp [this]
            use g; simp⟩
  else exact fintypeOfNotInfinite (fun h1 ↦ by aesop)

abbrev A : Fin 6 → Finset ℕ := fun i ↦ match i with
  | 1 => {1, 2}
  | 2 => {2, 3}
  | 3 => {3, 4}
  | 4 => {4, 5}
  | 5 => {5, 6}
  | 6 => {6, 1}

theorem brualdi_ch9_8 : Fintype.card (SDR A) = ((2) : ℕ ) := by sorry
Problem: Let $n>1$, and let $\mathcal{A}=\left(A_{1}, A_{2}, \ldots, A_{n}\right)$ be the family of subsets of $\{1,2, \ldots, n\}$, where \[ A_{i}=\{1,2, \ldots, n\}-\{i\}, \quad(i=1,2, \ldots, n) \] Prove that $\mathcal{A}$ has an SDR and that the number of SDRs is the $n$th derangement number $D_{n}$.

Lean formal statement:
import Mathlib

variable {α : Type*}

structure SDR {n : ℕ} (A : Fin n → Finset α) where
  toFun : Fin n → α
  mem_Ai : ∀ i, toFun i ∈ A i
  pairwise : ∀ i j, i ≠ j → toFun i ≠ toFun j

instance {n : ℕ} (A : Fin n → Finset α) : CoeFun (SDR A) (fun _ => Fin n → α) where
  coe s := s.toFun

noncomputable instance {n : ℕ} (A : Fin n → Finset α) : Fintype (SDR A) := by
  classical
  let Y := Finset.biUnion (@Finset.univ (Fin n) _) A
  if h : Nonempty (SDR A) then
    exact Fintype.ofSurjective (α := (Fin n → Y))
      (fun f ↦ if h1 : (∃(g : SDR A), ∀ i, f i = g i) then ⟨fun i => f i,
          fun i ↦ by have ⟨g, hg⟩ := h1; simp [hg, g.mem_Ai],
          fun i j hij ↦ by have ⟨g, hg⟩ := h1; simp [hg, g.pairwise i j hij]⟩
        else Classical.choice (α := (SDR A)) h) <| fun g ↦
          ⟨fun i => ⟨g i, by simp [Y]; use i; simp [g.mem_Ai]⟩, by
            simp; suffices ∃ (g' : SDR A), ∀ (i : Fin n), g.toFun i = g'.toFun i by simp [this]
            use g; simp⟩
  else exact fintypeOfNotInfinite (fun h1 ↦ by aesop)

theorem brualdi_ch9_11 (n : ℕ) (hn : n > 1) (A : Fin n → Finset ℕ)
    (hA : ∀ i, A i = Finset.Icc 1 n \ {i.1 + 1}) :
    Nonempty (SDR A) ∧ Fintype.card (SDR A) = numDerangements n := by sorry
Problem: Prove that $B = {0,3,4,9,11}$ is a difference set in $Z_{21}$.

Lean formal statement:
import Mathlib

def isDifferenceSet (n : ℕ) (B : Finset (ZMod n)) : Prop :=
  ∃ k, ∀ x : (ZMod n),  x ≠ 0 → ∑ i ∈ B, ∑ j ∈ B \ {i}, List.count x [i - j] = k

theorem brualdi_ch10_31 : isDifferenceSet 21 {0, 3, 4, 9, 11} := by sorry
Problem: Let $t$ be a positive integer. Prove that, if there exists a Steiner triple system of index 1 having $v$ varieties, then there exists a Steiner triple system having $v^{t}$ varieties.

Lean formal statement:
import Mathlib

structure SteinerTripleSystemOfIndOne (t k n : ℕ) where
  carrier : Fin n
  blocks : Finset (Finset (Fin n))
  card_blocks : ∀ b ∈ blocks, b.card = k
  block_inner : ∀ s : (Finset (Fin n)), s.card = t → ∃! b ∈ blocks, s ⊆ b

structure SteinerTripleSystem (t k n I : ℕ) where
  carrier : Fin n
  blocks : Finset (Finset (Fin n))
  card_blocks : ∀ b ∈ blocks, b.card = k
  block_inner : ∀ s : (Finset (Fin n)), s.card = t → ∃ f : Fin I ↪ blocks, ∀ i, s ⊆ f i

theorem brualdi_ch10_34 (t v : ℕ) (ht : t > 0) : Nonempty (SteinerTripleSystemOfIndOne 2 3 v) →
    ∃ I, Nonempty (SteinerTripleSystem 2 3 (v ^ t) I) := by sorry
Problem: Prove that a symmetric, idempotent Latin square has odd order.

Lean formal statement:
import Mathlib

structure LatinSquare (n : ℕ) where
  carrier : Matrix (Fin n) (Fin n) (ZMod n)
  pairwise_1 : ∀ i j1 j2, j1 ≠ j2 → carrier i j1 ≠ carrier i j2
  pairwise_2 : ∀ j i1 i2, i1 ≠ i2 → carrier i1 j ≠ carrier i2 j

def IsIdempotent {n : ℕ} (L : LatinSquare n) : Prop :=
  ∀ i, L.carrier i i = i

theorem brualdi_ch10_60 {n : ℕ} (hn : n > 0) (L : LatinSquare n) :
    IsIdempotent L ∧ L.1.IsSymm → Odd n := by sorry
Problem: Use the pigeonhole principle to prove that a graph of order n ≥ 2 always has two vertices of the same degree.

Lean formal statement:
import Mathlib

theorem brualdi_ch11_5 (n : ℕ) (h_n: n ≥ 2) (G : SimpleGraph (Fin n)) [DecidableRel G.Adj] :
    ∃ v1 v2, v1 ≠ v2 ∧ G.degree v1 = G.degree v2 := by sorry
Problem: Prove that the removal of an edge from a tree leaves a forest of two trees.

Lean formal statement:
import Mathlib

open SimpleGraph

theorem brualdi_ch11_59 {V : Type*} [Fintype V] [DecidableEq V]
    (T : SimpleGraph V) (hT : IsTree T) (e : Sym2 V) (he : e ∈ T.edgeSet) :
    ∃ (T1 T2 : SimpleGraph V), IsTree T1 ∧ IsTree T2 ∧
    T1.edgeSet ∪ T2.edgeSet = T.edgeSet \ {e} ∧
    Disjoint (T1.support) (T2.support) := by sorry
Problem: Prove that a graph of order n with at least `(n-1)(n-2)/2 + 1` edges must be connected.

Lean formal statement:
import Mathlib

theorem brualdi_ch11_20 {V : Type*} [Fintype V] (n : ℕ) (hn : n ≥ 1) (hV : Fintype.card V = n)
    (G : SimpleGraph V) (h : (n - 1) * (n - 2) / 2 + 1 ≤ (SimpleGraph.edgeSet G).ncard) :
    G.Connected := by sorry
Problem: Determine the domination number of the graph $Q_{3}$ of vertices and edges of a three-dimensional cube.
Answer: 2

Lean formal statement:
import Mathlib

open SimpleGraph BigOperators Classical

variable (n : ℕ) {V : Type*} (G : SimpleGraph V)

def SimpleGraph.IsDominatingSet (D : Set V) : Prop :=
  ∀ v : V, ¬ (v ∈ D) →  ∃ u ∈ D, G.Adj u v

lemma IsDominatingSet.univ : G.IsDominatingSet Set.univ := by simp [IsDominatingSet]

noncomputable def SimpleGraph.eDominationNum : ℕ∞ := iInf (fun s ↦ if
  (G.IsDominatingSet s) then s.card else ⊤ : (Finset V) → ℕ∞)

noncomputable def SimpleGraph.dominationNum : ℕ := G.eDominationNum.toNat

abbrev Q_3 := (pathGraph 2) □ (pathGraph 2) □ (pathGraph 2)

theorem brualdi_ch12_37 : Q_3.dominationNum = ((2) : ℕ ):= by sorry
Problem: Let $G$ be a graph. Prove that $G$ is 2-connected if and only if, for each vertex $x$ and each edge $\alpha$, there is a cycle that contains both the vertex $x$ and the edge $\alpha$.

Lean formal statement:
import Mathlib

structure TwoConnected {V : Type*} (G : SimpleGraph V) : Prop where
  selfconnected : G.Connected
  remains_connected : ∀ x : V, ((⊤ : SimpleGraph.Subgraph G).deleteVerts {x}).coe.Connected

theorem brualdi_ch12_62 {V : Type*} (G : SimpleGraph V) : TwoConnected G ↔ ∀ x : V, ∀ e ∈ G.edgeSet,
    ∃ G' : SimpleGraph.Subgraph G, x ∈ G'.verts ∧ e ∈ G'.edgeSet ∧ G'.coe.IsCycles := by sorry
Problem: Prove that the complement of a disconnected graph is connected.

Lean formal statement:
import Mathlib

theorem brualdi_ch12_34 {V : Type*} (G : SimpleGraph V) (h : ¬ G.Connected) :
    Gᶜ.Connected := by sorry