Compfiles/Imo1972P1.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

International Mathematical Olympiad 1972, Problem 1

Prove that from a set of ten distinct two-digit numbers (in decimal), it is possible to select two disjoint subsets whose members have the same sum.

Imports (2)
Imported by 1 file
  1. problem Imo1972P1.imo1972_p1 line 27 source

    standard axioms: Classical.choice, Quot.sound, propext what this means

    Statement uses: Finset, Nat, Eq, Finset.card, OfNat.ofNat, Membership.mem, List.length, Nat.digits, Exists, And, LE.le, Disjoint, Finset.sum

    Proof uses: Finset.Ico, LT.lt, Mathlib.Meta.NormNum.isNat_lt_true, Mathlib.Meta.NormNum.isNat_ofNat, Eq.refl, Bool, Bool.false, HPow.hPow, Nat.lt_base_pow_length_digits, Ne, False, False.elim, Eq.mp, Eq.trans, congrFun', congrArg, List, List.nil, Nat.digits_zero, eq_false and 36 more

    59 instances, coercions and auxiliary constants left out.

    Tactic trace: 66 steps

    Open to load the checked before-and-after goal states.