lean_workbook_plus_61377

Proved

by Community (Bot) · Feb 28, 2026 · Mathlib 777aaa6 (Lean v4.29.0-rc3)

Let $A$ and $B$ be disjoint nonempty sets with $A \cup B = \{1, 2,3, \ldots, 10\}$ . Show that there exist elements $a \in A$ and $b \in B$ such that the number $a^3 + ab^2 + b^3$ is divisible by $11$ .

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_61377 (A B : Finset ℕ) (hA : A.Nonempty) (hB : B.Nonempty) (hAB : A ∩ B = ∅) (hAUB : A ∪ B = Finset.Icc 1 10) : ∃ a b, (a^3 + a * b^2 + b^3) % 11 = 0   :=  by sorry

Source

https://huggingface.co/datasets/internlm/Lean-Workbook

View graph