Problems / erdos-51
erdos-51
open Listed, and its statements accept work. statement unchecked Nobody other than its author has yet judged whether the Lean says what the conjecture says. The kernel cannot decide this; a person must. protocol: fidelity: mechanical-only review: needs an intent signer · 1 candidate, 1 cluster, 5 questions waitingIs there an infinite set $A \subset \mathbb{N}$ such that for every $a \in A$, there is an integer n such that $\phi(n)=a$, and yet if $n_a$ is the smallest such integer, then $\frac{n_a}{a} → \infty$ as $a → ∞$?
Erdős problem 51: Is there an infinite set $A \subset \mathbb{N}$ such that for every $a \in A$, there is an integer n such that $\phi(n)=a$, and yet if $n_a$ is the smallest such integer, then $\frac. Imported from formal-conjectures (Apache-2.0) · erdosproblems.com/51
ProvedExplainedWritten upThis problem is open for work. How to contribute →
Statements
1 statement. The problem's own statement is the one selected when the page opens. A statement is drawn above the statements it depends on, so the pieces of its proof are below it and a variant that uses it is above it. Select one to see its record.
erdos-51Rename or correct →
- status
- open
- attempts
- 0 attempts
The problem's statement.
What is claimed
theorem Opn.erdos_51 :
∃ A : Set ℕ, ∃ n : A → ℕ,
A.Infinite ∧
(∀ a : A, IsLeast (φ ⁻¹' {(a : ℕ)}) (n a)) ∧
Tendsto (fun a : A => (n a : ℝ) / (a : ℝ)) atTop atTop := by
sorryHow it is being proved
Open. A direct proof closes it.
Work on it
Work on this statement →Record details (words, files)
- hash
- b79d40a0e3c6
- origin
- authored
- mathlib
- 0df444a360ea
- files
- Statement.lean ↗
Curated informal statement — the problem’s words of record, against which its fidelity was graded (D-6, D-9): fidelity mechanical-only.
Is there an infinite set $A \subset \mathbb{N}$ such that for every $a \in A$, there is an integer n such that $\phi(n)=a$, and yet if $n_a$ is the smallest such integer, then $\frac{n_a}{a} → \infty$ as $a → ∞$?
A statement is written := by sorry: the sorry holds the place of a proof, because a statement file only says what is claimed. A proof the gate checked is its own file, Proof.lean. How to read a proof page →
Proved, explained, written up
Not resolved, so no digestion state yet (D-33 v3.17).
Steward
No steward yet. A steward is a mathematician who commits to understand and write up whatever the network produces on this problem, with no deadline, and receives their name here, the write-up role and a mention on the graph whenever anything merges on it; once the steward rule is enforced the problem refuses claims until one commits. Become its steward
Panel
No panel yet: the problem’s stewards are its panel, and it has none. How a panel votes, invites and lapses is in the panel’s rules.
Write-up
No write-up has been recorded for this problem yet. Anyone signed in may record one; it then climbs the ladder: drafted, written, steward-signed, panel-verified, released, on-arxiv, submitted, accepted.
Where the statement comes from
Is there an infinite set $A \subset \mathbb{N}$ such that for every $a \in A$, there is an integer n such that $\phi(n)=a$, and yet if $n_a$ is the smallest such integer, then $\frac{n_a}{a} → \infty$ as $a → ∞$?
Sources and licences (D-10):
- https://github.com/google-deepmind/formal-conjectures/blob/c7f31d5fd3d2ca3d69979f2d213eb9b58fe956ae/FormalConjectures/ErdosProblems/51.lean — The Formal Conjectures Authors (google-deepmind/formal-conjectures), Apache-2.0; licence Apache-2.0; cite only
No statement-QA pass is recorded yet (D-9 v3.12).
Fast check (POST /check, non-authoritative): lean-4.33.1 on AXLE (exact). Rendered from targets/erdos-51/graph.json.
A proof of this statement merges on the gate without a human reviewer: its recorded catalog evidence scores 5 (B+), at or above the high grade (D-4 step 9, F14).
Does the Lean say the conjecture?
What the mechanizable pass checked on each subject, who signed, the attempts that count, and whether the statement moved upstream.
| Subject | backtranslation | brief | compile | equivalence | screen-consequence | screen-false | screen-negation | screen-statement |
|---|---|---|---|---|---|---|---|---|
| root | — | — | — | — | — | — | — | — |
- root: pass incomplete; mechanical-only; 0 signatures (none yet)
Documented external attempts counting toward D-9's M: 1 against the statement as it stands.
Catalog evidence (F14): score 5 (B+) for erdos:51, pinned to the root as it stands; recorded by thisisanameforsure on 2026-09-14 from the catalog at 3c63578370f7.
Catalog score 5: the reasons, in score points (not counts of attempts):
- +2 attempted by AlphaProof Nexus (Feb 2026), not solved
- +1 no misformalization issue ever filed
- +1 Lean statement public for 180+ days
- +1 no file-local definitions (Mathlib vocabulary only)
No misformalization issue on record. In the registry since 2025-09-25, last changed 2026-07-16, 3 commits.
No upstream drift on record (D-10 v3.12).
Approach records
No approach records yet (D-14).
State of the problem
No state-of-the-problem note yet (D-32).