## Compfiles: Catalog Of Math Problems Formalized In Lean

## UK2024R1P1

```
import Mathlib.Data.Set.Card
import Mathlib.Logic.Equiv.Defs
import Mathlib.Tactic
/-!
# British Mathematical Olympiad 2024, Round 1, Problem 1
An unreliable typist can guarantee that when they try to type a word with
different letters, every letter of the word will appear exactly once in what
they type, and each letter will occur at most one letter late (though it may
occur more than one letter early). Thus, when trying to type MATHS, the
typist may type MATHS, MTAHS or TMASH, but not ATMSH.
Determine, with proof, the number of possible spellings of OLYMPIADS
that might be typed.
-/
namespace UK2024R1P1
/- determine -/ abbrev solution_value : ℕ := sorry
/-
Since OLYMPIADS has no duplicate letters, then the set of spellings is just a
subset of the permutations of 9 elements.
-/
theorem uk2024_r1_p1 :
{f : Equiv.Perm (Fin 9) | ∀ k, (f k : ℕ) ≤ k + 1}.ncard = solution_value := sorry
end UK2024R1P1
```

File author(s): short_c1rcuit

This problem has a complete formalized solution.

Open with the in-brower editor at live.lean-lang.org: