philip_b comments on What are the best elementary math problems you know?

[philip_b]

I’ve formalized this problem in Coq with mathcomp. Yeah, idk why I decided to do this.

From mathcomp Require Import all_ssreflect.
Set Implicit Arguments.
Unset Strict Implicit.
Unset Printing Implicit Defensive.

Definition hats_assignment : Type := nat -> bool.

Definition policy_of_one_person (n : nat) : Type :=
  {policy : hats_assignment -> bool &
   forall ha : hats_assignment,
     let ha' := fun m => if m == n is true then ~~ (ha m) else ha m
     in policy ha == policy ha'}.

Definition strategy : Type :=
  forall n : nat, policy_of_one_person n.

Lemma ex_good_strategies :
  exists s : strategy, forall ha : hats_assignment, exists N : nat, forall n : nat, n >= N ->
    (projT1 (s n)) ha == ha n.
Proof.
Admitted.

If you want to solve it, you need to replace Admitted. with an actual proof.

[Ege Erdil]

This is great.