Erdős problem 138

In [Er80] Erdős asks whether

\lim_{k \to \infty} (W(k))^{1/k} = \infty

Withdrawn 6 Oct 2026

OWNER_ACCEPTED_PUBLICATION_CLOSURE (closed on the release owner's instruction of 2026-10-06T23:17:23Z to accept the public resolution claim in OpenAI math corpus family 160, commit adc7f1241b42e322a6451854ab7e4b4c146bf78a, first public 2026-10-06T21:58:50Z. Owner-directed acceptance: no independent proof replay or certification was performed. See OWNER-ACCEPTED-CLOSURES-2026-10-06.md.)

Formal statement

Proof target

import FormalConjectures.ErdosProblems.«138»
import TaskSupport

namespace Bounty

theorem target : fcTypeOfName% "Erdos138.erdos_138" := by
  sorry

end Bounty

Open this target’s Challenge.lean

Original conjecture (Lean type)

True ↔ Filter.Tendsto (fun k => ↑(Erdos138.W k) ^ (1 / ↑k)) Filter.atTop Filter.atTop

Original conjecture source: FormalConjectures/ErdosProblems/138.lean

Task id: fc-6a786f99-erdos138-erdos-138-1ef589ced9-formalized-v1
Task commitment: sha256:caf8d2ff33806dee54aeddd39e78669c95e62d085495d7ff4d9d144dad744df4

References

erdosproblems.com/138

[Be68] Berlekamp, E. R., A construction for partitions which avoid long arithmetic progressions. Canad. Math. Bull. (1968), 409-414.
[Er80] Erdős, Paul, A survey of problems in combinatorial number theory. Ann. Discrete Math. (1980), 89-115.
[Er81] Erdős, P., On the combinatorial problems which I would most like to see solved. Combinatorica (1981), 25-42.
[Go01] Gowers, W. T., A new proof of Szemerédi's theorem. Geom. Funct. Anal. (2001), 465-588.

Something wrong with this formalization?

A statement that does not faithfully capture the original conjecture is the one real risk here, so we would rather hear about it early - before someone spends weeks on it.

Our channel is in the Bittensor Discord server. Join the server first, then open the channel to send your report.

Join Bittensor Discord

Erdős problem 138

In [Er80] Erdős asks whether

\lim_{k \to \infty} (W(k))^{1/k} = \infty

Withdrawn 6 Oct 2026