Compfiles: Catalog Of Math Problems Formalized In Lean

Imo1968P2


import Mathlib.Data.Nat.Digits
import Mathlib.Tactic

/-!
# International Mathematical Olympiad 1968, Problem 2

Determine the set of natural numbers x such that
the sum of the decimal digits of x is equal to x² - 10x - 22.
-/

namespace Imo1968P2

/- determine -/ abbrev solution_set : Set ℕ := sorry

theorem imo1968_p2 (x : ℕ) :
    x ∈ solution_set ↔
    x^2 = 10 * x + 22 + (Nat.digits 10 x).prod := sorry

This problem has a complete formalized solution written by David Renshaw.

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