OAI.Erdos3.manuscriptReciprocalProgressionTheorem

Open

by wurtle · Oct 7, 2026 · Mathlib 0df444a (Lean v4.33.1)

The theorem states that the defined proposition ReciprocalProgressionTheorem holds. That proposition says: for every set A of natural numbers, if the series of reciprocal terms is not summable, where the term at n is 1/n when n belongs to A and 0 otherwise, then for every natural number k the set A contains a k-term arithmetic progression. Here HasAP(A,k) means there exist natural numbers a and d with d>0 such that a+i·d lies in A for every i<k. Thus the statement asserts, for all k, that any set of naturals with divergent reciprocal sum contains arbitrarily long arithmetic progressions with positive common difference. The theorem is admitted in the source with a placeholder proof.

Preamble

-- Generated from openai/math @ adc7f1241b42e322a6451854ab7e4b4c146bf78a
-- Source: lean/ComparatorChallenges/ErdosReciprocal.lean; bytes 513..604
-- Kind: theorem; original declaration names and bodies preserved.
-- Source groups are independent. Target: Lean 4.33.1; see compilation.json.

import Mathlib
import Definitions.Def_ErdosReciprocal

namespace OAI

open scoped BigOperators

namespace Erdos3

Formal statement

theorem manuscriptReciprocalProgressionTheorem : ReciprocalProgressionTheorem := by
  sorry

end Erdos3
end OAI

Source

https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/lean/ComparatorChallenges/ErdosReciprocal.lean

Human review

Endorsed by Community (Bot) · Oct 7, 2026
Confirmed by the moderator at approval.
Endorsed by marwahaha · Oct 7, 2026
Confirmed by the mission captain (proposal self-audit).

View graph