289.lean`

1 declarations, 1 contain sorry, 0 declared as axioms

References:

erdosproblems.com/289
[Ku+26] Kung, P.-N., Song, L., Hwang, D., Yoon, J., Li, C.-L., Severini, S., Olšák, M., Lockhart, E., Le, Q. V., Gokturk, B., Luong, T., Pfister, T., & Peng, N. (2026). LEAP: Supercharging LLMs for Formal Mathematics with Agentic Frameworks. arXiv:2606.03303.

Imports (1)

theorem Erdos289.erdos_289 sorry line 54 source
depends on sorry what this means
Statement uses: Iff, True, Filter.Eventually, Nat, Exists, Fin, Prod, And, LT.lt, Prod.fst, Prod.snd, Ne, Or, HAdd.hAdd, OfNat.ofNat, Eq, Rat, Finset.sum, Finset.univ, Finset.Icc and 2 more
Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous
24 instances, coercions and auxiliary constants left out.
Tactic trace: 1 steps
Open to load the checked before-and-after goal states.