## Compfiles: Catalog Of Math Problems Formalized In Lean

## Imo1973P5

```
import Mathlib.Tactic
/-!
# International Mathematical Olympiad 1973, Problem 5
$G$ is a set of non-constant functions of the real variable $x$ of the form
\[f(x) = ax + b, a \text{ and } b \text{ are real numbers,}\] and $G$ has the following properties:
(a) If $f$ and $g$ are in $G$, then $g \circ f$ is in $G$; here $(g \circ f)(x) = g[f(x)]$.
(b) If $f$ is in $G$, then its inverse $f^{-1}$ is in $G$;
here the inverse of $f(x) = ax + b$ is $f^{-1}(x) = (x - b) / a$.
(c) For every $f$ in $G$, there exists a real number $x_f$ such that $f(x_f) = x_f$.
Prove that there exists a real number $k$ such that $f(k) = k$ for all $f$ in $G$.
-/
namespace Imo1973P5
theorem imo1973_p5 {G : Set (ℝ → ℝ)}
(hf: ∀ f ∈ G, ∃ a b : ℝ, a ≠ 0 ∧ ∀ x : ℝ, f x = a * x + b)
(hG : ∀ f ∈ G, ∀ g ∈ G, g ∘ f ∈ G)
(hinv : ∀ f ∈ G, (∀ x, f x ≠ 0) → f⁻¹ ∈ G)
(hfix : ∀ f ∈ G, ∃ x, f x = x) :
∃ k : ℝ, ∀ f ∈ G, f k = k := sorry
end Imo1973P5
```

File author(s): InternLM-MATH LEAN Formalizer v0.1

This problem does not yet have a complete formalized solution.

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