Compfiles: Catalog Of Math Problems Formalized In Lean

Imo1979P6

import Mathlib

/-!
# International Mathematical Olympiad 1979, Problem 6

Let $A$ and $E$ be opposite vertices of an octagon.
A frog starts at vertex $A.$ From any vertex except $E$ it jumps to one of the two adjacent vertices.
When it reaches $E$ it stops. Let $a_n$ be the number of distinct paths of exactly $n$ jumps ending at $E$.
Prove that: \[a_{2n-1}=0, \quad a_{2n}={(2+\sqrt2)^{n-1} - (2-\sqrt2)^{n-1} \over\sqrt2}.\]
-/

namespace Imo1979P6

open SimpleGraph

abbrev Octagon := cycleGraph 8
abbrev A : Fin 8 := 0
abbrev E : Fin 8 := 4

def isTerminalWalk {V : Type} {G : SimpleGraph V} {u v : V} (w : G.Walk u v) := v ∉ w.support.dropLast

noncomputable def a (n : ℕ) := Set.ncard {w : Octagon.Walk A E | isTerminalWalk w ∧ w.length = n}


theorem imo1979_p6 (n : ℕ) (npos : 0 < n) : a (2*n-1) = 0 ∧ a (2*n) = ((2+√2)^(n-1) - (2-√2)^(n-1)) / √2 := sorry

end Imo1979P6

File author(s): Constantin Seebach

This problem has a complete formalized solution.