← problemsEP0014openMathematics/ Number theory

Erdős Problem 266

Let $a_n$ be an infinite sequence of positive integers such that $\sum \frac{1}{a_n}$ converges. There exists some integer $t \ge 1$ such that $\sum \frac{1}{a_n + t}$ is irrational. This was disproven by Kovač and Tao in [KoTa24]. [KoTa24] Kovač, V. and Tao T., On several irrationality problems for Ahmes series. arXiv:2406.17593 (2024).

▸Motivation

Recorded upstream as solved in the literature, but no Lean proof exists here yet. It is listed as open because nothing on this site is marked solved without a proof the kernel accepts — a known result needing formalization is a tractable task, and a good place to start.

Adapted from formal-conjectures, ErdosProblems/266.lean. Catalogued at https://www.erdosproblems.com/266.

▸Lean API

import Mathlib.NumberTheory.Real.Irrational

namespace Conjectura.EP0014

/-- Let $a_n$ be an infinite sequence of positive integers such that $\sum \frac{1}{a_n}$ converges. There exists some integer $t \ge 1$ such that $\sum \frac{1}{a_n + t}$ is irrational. This was disproven by Kovač and Tao in [KoTa24]. [KoTa24] Kovač, V. and Tao T., On several irrationality problems for Ahmes series. [arXiv:2406.17593](https://arxiv.org/abs/2406.17593) (2024). -/
def goal : Prop :=
  ¬ ∀ (a : ℕ → ℕ), ((∀ n : ℕ, a n ≥ 1) ∧ Summable ((1 : ℝ) / a ·) →
      ∃ t ≥ (1 : ℕ), Irrational <| ∑' n, (1 : ℝ) / ((a n) + t))

end Conjectura.EP0014

▸Definition1

IrrationalIrrational: def

Download the Lean definitions

▸Related work2

Erdős Problem 266Thomas Bloom (catalogue)
The catalogue entry, with references and status.
formal-conjecturesThe Formal Conjectures Authors (Google DeepMind) · 2025
Source of the Lean formalization adapted here.

▸For your AI

Download as .md

I am proving a theorem in Lean 4 and submitting it to Conjectura.

## Problem EP0014 — Erdős Problem 266

Let $a_n$ be an infinite sequence of positive integers such that $\sum \frac{1}{a_n}$ converges. There exists some integer $t \ge 1$ such that $\sum \frac{1}{a_n + t}$ is irrational. This was disproven by Kovač and Tao in [KoTa24]. [KoTa24] Kovač, V. and Tao T., On several irrationality problems for Ahmes series. [arXiv:2406.17593](https://arxiv.org/abs/2406.17593) (2024).

## Environment (fixed — do not assume anything newer)

- Lean toolchain: `leanprover/lean4:v4.33.0-rc1`
- Mathlib: `v4.33.0-rc1`

If a lemma you want does not exist in that Mathlib, prove it inline instead of
importing something newer.

## The exact statement I must prove

```lean
theorem solution : Conjectura.EP0014.goal := by
  sorry
```

## The file I submit

```lean
import Conjectura.Problems.EP0014.Statement

namespace Submission

theorem solution : Conjectura.EP0014.goal := by
  sorry

end Submission

```

## The Lean definitions of every term in this problem

These are the actual definitions your proof will be checked against. Do not
substitute your own version of any of them.

### Irrational

def

```lean
Irrational
```
Defined in Mathlib.

## Rules — submissions violating these are rejected automatically

1. **Do not change the name or type of `solution`.** It must satisfy the
   statement above exactly.
2. **Do not redefine or shadow anything from the problem's Statement module.**
   Declaring your own `goal`, or redefining a name it depends on, produces a
   proof of a *different* statement and is rejected. This is the single most
   common rejection.
3. **No `sorry`** anywhere, including in helper lemmas. It surfaces as the
   axiom `sorryAx` and is detected transitively through imports.
4. **No `native_decide`** — it surfaces as `Lean.ofReduceBool` and is not
   accepted, because it trusts compiled code rather than the kernel.
5. Only these axioms are permitted: `propext`, `Classical.choice`,
   `Quot.sound`.
6. Follow Mathlib style: hypotheses left of the colon, explicit types,
   `snake_case` theorem names, `UpperCamelCase` types.

## What I want from you

Here is my argument in informal mathematics:

> [PASTE YOUR PROOF SKETCH HERE]

Turn it into Lean 4 that compiles under the environment above and satisfies the
statement exactly. Where you are unsure a lemma exists in this Mathlib version,
say so explicitly rather than guessing a name.

Submissions are not open yet

Conjectura is in beta. You can read every statement, every definition and the Lean behind them, and download the exact files the checker uses — but proofs are not being accepted yet.

The reason is a deliberate order of operations. Accepting a proof means running a stranger’s code and standing behind a verdict, and no statement here yet carries a researcher’s name. A machine-checked answer to a question nobody has vouched for is worth very little, so the vouching comes first.

Maintain a subject area Download the Lean for this problem

The English write-ups are also switched off during the beta. Nothing on this page is generated by a model.

Discussion

Nothing yet.