City Zhautykov 2024 Grade 8 Problem 2

Positive real numbers $a, b, c, d$ are such that all $$ab, bc, cd, da, ac, bd, abc, abd, acd, bcd, abcd$$ are integers. Is it the case that at least one of $a, b, c, d$ must be an integer?

Replace sorry in the template below with your solution. See Answer Bank for acceptible answer declarations. Mathlib version used by the checker is v4.29.0. 

import Mathlib.Data.Real.Basic

def P (a b c d : ℝ) := 0 < a ∧ 0 < b ∧ 0 < c ∧ 0 < d ∧
    (∃ n : ℤ, n = a * b) ∧ (∃ n : ℤ, n = b * c) ∧ (∃ n : ℤ, n = c * d) ∧
    (∃ n : ℤ, n = d * a) ∧ (∃ n : ℤ, n = a * c) ∧ (∃ n : ℤ, n = b * d) ∧
    (∃ n : ℤ, n = a * b * c) ∧ (∃ n : ℤ, n = a * b * d) ∧
    (∃ n : ℤ, n = a * c * d) ∧ (∃ n : ℤ, n = b * c * d) ∧
    (∃ n : ℤ, n = a * b * c * d)

def answer : Prop := sorry

theorem solution : (∀ a b c d, P a b c d → ∃ n : ℤ, n = a ∨ n = b ∨ n = c ∨ n = d) ↔ answer := sorry

Submit Solution

Login to submit a solution.

Recent Submissions

# User Time (UTC) Status
312 Otabek_Aynazarov 2026-03-01T05:08 Forbidden axiom ⓘ
223 FelixMP Long time ago PASSED ⓘ
182 Kitsune Long time ago PASSED ⓘ
View all