Number theory

Erdős problem 291 - part i

Let

n\geq 1

and define

L_n

to be the least common multiple of

\{1,\ldots,n\}

and

a_n

\sum_{1\leq k\leq n}\frac{1}{k}=\frac{a_n}{L_n}

. Is it true that

(a_n,L_n)=1

occurs for infinitely many

n

$5,101 bounty1 piece from 1 personlast one last month

week of 17 Oct 2025 · nothing publishedweek of 24 Oct 2025 · nothing publishedweek of 31 Oct 2025 · nothing publishedweek of 7 Nov 2025 · nothing publishedweek of 14 Nov 2025 · nothing publishedweek of 21 Nov 2025 · nothing publishedweek of 28 Nov 2025 · nothing publishedweek of 5 Dec 2025 · nothing publishedweek of 12 Dec 2025 · nothing publishedweek of 19 Dec 2025 · nothing publishedweek of 26 Dec 2025 · nothing publishedweek of 2 Jan 2026 · nothing publishedweek of 9 Jan 2026 · nothing publishedweek of 16 Jan 2026 · nothing publishedweek of 23 Jan 2026 · nothing publishedweek of 30 Jan 2026 · nothing publishedweek of 6 Feb 2026 · nothing publishedweek of 13 Feb 2026 · nothing publishedweek of 20 Feb 2026 · nothing publishedweek of 27 Feb 2026 · nothing publishedweek of 6 Mar 2026 · nothing publishedweek of 13 Mar 2026 · nothing publishedweek of 20 Mar 2026 · nothing publishedweek of 27 Mar 2026 · nothing publishedweek of 3 Apr 2026 · nothing publishedweek of 10 Apr 2026 · nothing publishedweek of 17 Apr 2026 · nothing publishedweek of 24 Apr 2026 · nothing publishedweek of 1 May 2026 · nothing publishedweek of 8 May 2026 · nothing publishedweek of 15 May 2026 · nothing publishedweek of 22 May 2026 · nothing publishedweek of 29 May 2026 · nothing publishedweek of 5 Jun 2026 · nothing publishedweek of 12 Jun 2026 · nothing publishedweek of 19 Jun 2026 · nothing publishedweek of 26 Jun 2026 · nothing publishedweek of 3 Jul 2026 · nothing publishedweek of 10 Jul 2026 · nothing publishedweek of 17 Jul 2026 · nothing publishedweek of 24 Jul 2026 · nothing publishedweek of 31 Jul 2026 · nothing publishedweek of 7 Aug 2026 · nothing publishedweek of 14 Aug 2026 · nothing publishedweek of 21 Aug 2026 · nothing publishedweek of 28 Aug 2026 · 1 piece publishedweek of 4 Sept 2026 · nothing publishedweek of 11 Sept 2026 · nothing publishedweek of 18 Sept 2026 · nothing publishedweek of 25 Sept 2026 · nothing publishedweek of 2 Oct 2026 · nothing publishedweek of 9 Oct 2026 · nothing published

17 Oct 2025a year of work on this problem9 Oct 2026

Solve it

Nobody has attempted this. A complete proof or refutation takes the whole bounty.

Submit a proof

Add a piece

A lemma, a definition, a special case. There is no race: when someone finishes the problem, the pool splits between everyone whose work led there.

contrib new erdos-291-parts-i

Command line, then a pull request on GitHub.

What has been built

1 piece · 5 lemmas

1 Sept 2026
- Infinitely many n with gcd(a(n), lcm(1..n)) > 1
  5FqLp5…FfZZiK · 5 lemmas

Where this lives

conjectures-tasks

The pinned statement, the Lean challenge file and the exact bundle you build against.

pool/tier-1/erdos-291-parts-i-formalized →

conjectures-contribution

Every published piece for this problem, with its Lean source and its signed record.

contributions/erdos-291-parts-i →

Formal statement

Proof target

import FormalConjectures.ErdosProblems.«291»
import TaskSupport

namespace Bounty

theorem target : fcTypeOfName% "Erdos291.erdos_291.parts.i" := by
  sorry

end Bounty

Open this target’s Challenge.lean

Original conjecture (Lean type)

True ↔ {n | (Erdos291.a n).gcd (Erdos291.L n) = 1}.Infinite

Original conjecture source: FormalConjectures/ErdosProblems/291.lean

Source type SHA-256: sha256:03a93b18e4006002588bf9dc58264328a2a202ac494b5dcd84c8356f558dfd3a
Task id: fc-4b69a7dc-parts-i-a65d6c3db8-formalized-v1
Task commitment: sha256:3f272e63043fc416419409ecaf155f16fb5c31dfe654cf5f3a8fc33bc92d6810

References

erdosproblems.com/291

[ErGr80, p.34] Erdős, P. and Graham, R., Old and new problems and results in combinatorial number theory. Monographies de L'Enseignement Mathematique (1980).
[Sh16] P. Shiu, The denominators of harmonic numbers. arXiv:1607.02863 (2016).
[WuYa22] Wu, Bing-Ling and Yan, Xiao-Hui, On the denominators of harmonic numbers. {IV}. C. R. Math. Acad. Sci. Paris (2022), 53--57.

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