Open Proof Network

Problems / erdos-417

erdos-417

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, 8 questions waiting

Let$$V'(x)=\#\{\phi(m) : 1\leq m\leq x\}$$and$$V(x)=\#\{\phi(m) \leq x : 1\leq m\}.$$ Does $\lim V(x)/V'(x)$ exist?

Erdős problem 417, part i: Let$$V'(x)=\#\{\phi(m) : 1\leq m\leq x\}$$and$$V(x)=\#\{\phi(m) \leq x : 1\leq m\}.$$ Does $\lim V(x)/V'(x)$ exist? Imported from formal-conjectures (Apache-2.0) · erdosproblems.com/417

ProvedExplainedWritten up

This 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.

proved A proof passed all nine checks and was merged. Proved is not the same as explained. protocol: proved open No proof has closed this statement and nothing blocks starting on it. Anyone may work on it now. protocol: ready · on the frontier blocked Waits on other statements, or on a definition that has not been checked yet. Not accepting work. A statement waiting only for its witness is not blocked in this sense: it needs a witness. protocol: blocked
erdos-417 (Erdős problem 417, part i): ready Erdős problem 417, part i
labels drop the problem’s own name (a pill’s title has its full id); hovertap a statement to light its lines; select a set in the tree above to see its tree here
Selected statement Erdős problem 417, part i

erdos-417Rename or correct →

status
open
attempts
0 attempts

The problem's statement.

What is claimed

theorem Opn.erdos_417 :
    ∃ L : ENNReal, Tendsto (fun x ↦
      ({ k | k ∈ range totient ∧ (k : ℝ) ≤ x }.ncard : ENNReal) /
      ((totient '' { m | 1 ≤ m ∧ (m : ℝ) ≤ x }).ncard : ENNReal))
      atTop (𝓝 L) := by
  sorry

Explain this →

How it is being proved

Open. A direct proof closes it.

Work on it

Work on this statement →
Record details (words, files)
hash
a7c738be851d
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.

Let$$V'(x)=\#\{\phi(m) : 1\leq m\leq x\}$$and$$V(x)=\#\{\phi(m) \leq x : 1\leq m\}.$$ Does $\lim V(x)/V'(x)$ exist?

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 →

How to read this →

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

Let$$V'(x)=\#\{\phi(m) : 1\leq m\leq x\}$$and$$V(x)=\#\{\phi(m) \leq x : 1\leq m\}.$$ Does $\lim V(x)/V'(x)$ exist?

Sources and licences (D-10):

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-417/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.

Subjectbacktranslationbriefcompileequivalencescreen-consequencescreen-falsescreen-negationscreen-statement
root————————

Documented external attempts counting toward D-9's M: 2 against the statement as it stands.

Catalog evidence (F14): score 5 (B+) for erdos:417, 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 2026-01-22, last changed 2026-08-05, 7 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).