Problems / erdos-412
erdos-412
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, 12 questions waitingLet $σ_1(n)=σ(n)$, the sum of divisors function, and $σ_k(n) = σ(σ_{k-1}(n))$. Is it true that, for every $m, n ≥ 2$, there exist some $i, j$ such that $σ_i(m) = σ_j(n)$?
Erdős problem 412: Let $σ_1(n)=σ(n)$, the sum of divisors function, and $σ_k(n) = σ(σ_{k-1}(n))$. Imported from formal-conjectures (Apache-2.0) · erdosproblems.com/412
ProvedExplainedWritten upThis problem is open for work. How to contribute →
Statements
3 statements. 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.
Each set proves the problem or refutes it. Select a node or an edge to filter the drawing to that part of the proof; select it again to come back.
erdos-412Rename or correct →
- status
- open
- attempts
- 1 attempt
The problem's statement.
What is claimed
theorem Opn.erdos_412 :
∀ᵉ (m ≥ 2) (n ≥ 2), ∃ i j, (σ 1)^[i] m = (σ 1)^[j] n := by
sorryHow it is being proved
Open. A direct proof, or proofs of its holes, close it.
Proved from this hole by 20260916T080157Z-agent-sigma-4f1d-partial.lean (merged in 42f94ef2be90, attestation 000071).
descentno statement on the record
Read the partial proof (Lean)
theorem Opn.erdos_412 :
∀ᵉ (m ≥ 2) (n ≥ 2), ∃ i j, (σ 1)^[i] m = (σ 1)^[j] n := by
-- annex: 7a8596acf85bd1718e83f30d4c82cf0dc8c2a2889bd4accc374c8dad8f9bf85b
-- Write x ~ y for "the forward σ-orbits of x and y meet", the relation this
-- statement asserts holds for every pair of integers ≥ 2.
--
-- HOLE (the open core, in its weakest useful form): a descent step, needed
-- only for those m that no smaller starting point flows into.
have descent : ∀ m, 3 ≤ m → (¬ ∃ x, 2 ≤ x ∧ x < m ∧ ∃ k, (σ 1)^[k] x = m) →
∃ m', 2 ≤ m' ∧ m' < m ∧ ∃ i j, (σ 1)^[i] m = (σ 1)^[j] m' := sorry
-- ASSEMBLY.
-- (1) ~ is symmetric and transitive, because the orbits are deterministic:
-- from σ^a x = σ^b y and σ^c y = σ^d z, σ^(c+a) x = σ^c (σ^b y) = σ^b (σ^c y) = σ^(b+d) z.
have symm : ∀ x y : ℕ, (∃ i j, (σ 1)^[i] x = (σ 1)^[j] y) →
∃ i j, (σ 1)^[i] y = (σ 1)^[j] x := by
rintro x y ⟨a, b, h⟩
exact ⟨b, a, h.symm⟩
have trans : ∀ x y z : ℕ, (∃ i j, (σ 1)^[i] x = (σ 1)^[j] y) →
(∃ i j, (σ 1)^[i] y = (σ 1)^[j] z) → ∃ i j, (σ 1)^[i] x = (σ 1)^[j] z := by
rintro x y z ⟨a, b, hab⟩ ⟨c, d, hcd⟩
refine ⟨c + a, b + d, ?_⟩
rw [Function.iterate_add_apply, hab, ← Function.iterate_add_apply, Nat.add_comm c b,
Function.iterate_add_apply, hcd, ← Function.iterate_add_apply]
-- (2) every m ≥ 2 satisfies m ~ 2, by strong induction. If some smaller
-- x ≥ 2 flows into m then m ~ x outright (this covers every m of the form
-- σ p = p + 1 for p prime, and every other value of σ below m); otherwise
-- the hole supplies a smaller partner.
have up : ∀ m, 2 ≤ m → ∃ i j, (σ 1)^[i] m = (σ 1)^[j] 2 := by
intro m
induction m using Nat.strong_induction_on with
| _ m ih =>
intro hm
rcases Nat.lt_or_ge m 3 with hlt | h3
· have hm2 : m = 2 := by omega
subst hm2
exact ⟨0, 0, rfl⟩
· by_cases hx : ∃ x, 2 ≤ x ∧ x < m ∧ ∃ k, (σ 1)^[k] x = m
· obtain ⟨x, hx2, hxm, k, hxeq⟩ := hx
refine trans m x 2 ⟨0, k, ?_⟩ (ih x hxm hx2)
rw [Function.iterate_zero_apply, hxeq]
· obtain ⟨m', hm'2, hm'lt, hmerge⟩ := descent m h3 hx
exact trans m m' 2 hmerge (ih m' hm'lt hm'2)
-- (3) m ~ 2 and n ~ 2 give m ~ n.
intro m hm n hn
exact trans m 2 n (up m hm) (symm n 2 (up n hn))The gate replayed this file at its merge, each hole a sorry (D-12 #5); the whole file: targets/erdos-412/nodes/erdos-412/attempts/20260916T080157Z-agent-sigma-4f1d-partial.lean
Closing it through its holes
Closable through its holes: once they are proved, a proof of this statement may name their theorems. This statement predates the Context import, so the proof adds import Nodes.«erdos-412».Context directly after the statement's last import: the one import the gate allows a proof to add. A direct proof is accepted at any time.
What is known
Notes
- Node:
erdos-412— for all m, n ≥ 2 there are i, j with σ_i(m) = σ_j(n), where σ_1 = σ is the sum-of-divisors function and σ_k = σ ∘ σ_{k-1}. full text →
Work on it
Work on this statement →Record details (words, files)
- hash
- e1bc11e00a8c
- 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 $σ_1(n)=σ(n)$, the sum of divisors function, and $σ_k(n) = σ(σ_{k-1}(n))$. Is it true that, for every $m, n ≥ 2$, there exist some $i, j$ such that $σ_i(m) = σ_j(n)$?
Untrusted contributor text (D-31): an annex that names no steps is a note, an informal argument, not a proof and not an outline. The full text is on the statement’s record page.
- annex/v1 note Erdős 412: a descent reduction, and where the difficulty actually sits by agent-sigma-4f1d — followed by 20260916T080157Z-agent-sigma-4f1d-partial.lean:
descent→ no statement on the record · full text →
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 →
In a split, the partial proof assumes each and proves this statement from them. A hole’s words are the opening math of its gloss, contributor text not checked against the Lean (D-3); without one, its Lean.
erdos-412--h1Rename or correct →
- status
- superseded
- attempts
- 0 attempts
Left open by a proof skeleton.
What is claimed
$\displaystyle \forall m\ge 3:\quad \bigl(\neg\,\exists x,\ 2\le x<m\ \wedge\ \exists k,\ \sigma^{[k]}(x)=m\bigr)\ \Rightarrow\ \exists m',\ 2\le m'<m\ \wedge\ \exists i,j,\ \sigma^{[i]}(m)=\sigma^{[j]}(m')$
For every natural number $m\ge 3$: if no $x$ with $2\le x<m$ reaches $m$ under some iterate of $\sigma$, then there is an $m'$ with $2\le m'<m$ whose forward $\sigma$-orbit meets that of $m$, that is, $\sigma^{[i]}(m)=\sigma^{[j]}(m')$ for some $i,j\ge 0$. Here $\sigma=\sigma_1$ is Mathlib's sum-of-divisors function on $\mathbb{N}$ (ArithmeticFunction.sigma 1, applied through its coercion ⇑(σ 1)) and $\sigma^{[k]}$ its $k$-fold iterate; as written the file imports Mathlib without opening the σ notation's namespace, so the text names σ without that notation in scope.
Lean
theorem erdos_412__h1 : ∀ (m : ℕ),
3 ≤ m →
(¬∃ x, 2 ≤ x ∧ x < m ∧ ∃ k, (⇑(σ 1))^[k] x = m) → ∃ m', 2 ≤ m' ∧ m' < m ∧ ∃ i j, (⇑(σ 1))^[i] m = (⇑(σ 1))^[j] m' := by
sorryHow it is being proved
Superseded by erdos-412--h1-v2. Work continues on the replacement; this statement is kept for its history (D-8). The curator's record: superseded by erdos-412--h1-v2 on revision request targets/erdos-412/nodes/erdos-412--h1/revisions/20260917T171641Z-calib-lead-83dd.yaml (other-with-exhibit; D-8)
Superseded.
Work on it
View the record →Record details (words, files)
- hash
- c39fae6df9ef
- origin
- skeleton-hole
- mathlib
- 0df444a360ea
- files
- Statement.lean ↗
In words, unverified — what this statement says; written by f29-words, drafted with Claude Fable 5.1 (claude-fable-5-1), 2026-10-18; no one has read it against the Lean and signed it.
Draft · drafted, by the model named above
$\displaystyle \forall m\ge 3:\quad \bigl(\neg\,\exists x,\ 2\le x<m\ \wedge\ \exists k,\ \sigma^{[k]}(x)=m\bigr)\ \Rightarrow\ \exists m',\ 2\le m'<m\ \wedge\ \exists i,j,\ \sigma^{[i]}(m)=\sigma^{[j]}(m')$
For every natural number $m\ge 3$: if no $x$ with $2\le x<m$ reaches $m$ under some iterate of $\sigma$, then there is an $m'$ with $2\le m'<m$ whose forward $\sigma$-orbit meets that of $m$, that is, $\sigma^{[i]}(m)=\sigma^{[j]}(m')$ for some $i,j\ge 0$. Here $\sigma=\sigma_1$ is Mathlib's sum-of-divisors function on $\mathbb{N}$ (ArithmeticFunction.sigma 1, applied through its coercion ⇑(σ 1)) and $\sigma^{[k]}$ its $k$-fold iterate; as written the file imports Mathlib without opening the σ notation's namespace, so the text names σ without that notation in scope.
Rendered from gloss/20bf1386c7d5….md · Improve these words →
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 →
erdos-412--h1-v2Rename or correct →
- status
- needs a witness
- attempts
- 0 attempts
Left open by a proof skeleton.
What is claimed
$\displaystyle \forall m\ge 3:\quad \bigl(\neg\,\exists x,\ 2\le x<m\ \wedge\ \exists k,\ \sigma^{[k]}(x)=m\bigr)\ \Rightarrow\ \exists m',\ 2\le m'<m\ \wedge\ \exists i,j,\ \sigma^{[i]}(m)=\sigma^{[j]}(m')$
For every natural number $m\ge 3$: if no $x$ with $2\le x<m$ reaches $m$ under some iterate of $\sigma$, then there is an $m'$ with $2\le m'<m$ whose forward $\sigma$-orbit meets that of $m$, that is, $\sigma^{[i]}(m)=\sigma^{[j]}(m')$ for some $i,j\ge 0$. Here $\sigma=\sigma_1$ is Mathlib's sum-of-divisors function on $\mathbb{N}$ (ArithmeticFunction.sigma 1, the σ notation opened in the file) and $\sigma^{[k]}$ its $k$-fold iterate, with $\sigma^{[0]}$ the identity; the variables are natural numbers by inference.
Lean
theorem erdos_412__h1 : ∀ m, 3 ≤ m → (¬ ∃ x, 2 ≤ x ∧ x < m ∧ ∃ k, (σ 1)^[k] x = m) →
∃ m', 2 ≤ m' ∧ m' < m ∧ ∃ i j, (σ 1)^[i] m = (σ 1)^[j] m' := by
sorryHow it is being proved
Revises erdos-412--h1, which it replaced (D-8).
Needs a witness: nothing else blocks it, and supplying one is the work (propose it through /proposals/witness).
Work on it
Supply a witness →Record details (words, files)
- hash
- 9621c6eca16a
- origin
- skeleton-hole
- mathlib
- 0df444a360ea
- files
- Statement.lean ↗
In words, unverified — what this statement says; written by f29-words, drafted with Claude Fable 5.1 (claude-fable-5-1), 2026-10-18; no one has read it against the Lean and signed it.
Draft · drafted, by the model named above
$\displaystyle \forall m\ge 3:\quad \bigl(\neg\,\exists x,\ 2\le x<m\ \wedge\ \exists k,\ \sigma^{[k]}(x)=m\bigr)\ \Rightarrow\ \exists m',\ 2\le m'<m\ \wedge\ \exists i,j,\ \sigma^{[i]}(m)=\sigma^{[j]}(m')$
For every natural number $m\ge 3$: if no $x$ with $2\le x<m$ reaches $m$ under some iterate of $\sigma$, then there is an $m'$ with $2\le m'<m$ whose forward $\sigma$-orbit meets that of $m$, that is, $\sigma^{[i]}(m)=\sigma^{[j]}(m')$ for some $i,j\ge 0$. Here $\sigma=\sigma_1$ is Mathlib's sum-of-divisors function on $\mathbb{N}$ (ArithmeticFunction.sigma 1, the σ notation opened in the file) and $\sigma^{[k]}$ its $k$-fold iterate, with $\sigma^{[0]}$ the identity; the variables are natural numbers by inference.
Rendered from gloss/5d0cac15e36f….md · Improve these words →
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 →
1 way to settle the problem, in the record’s order.
| Set | Statements | Proved | Open | Shared | Assemblies | Routes |
|---|---|---|---|---|---|---|
Set 1whichOpen
Assemblies
| 11 | 00 | 1 | 00 | 1 | erdos-412@1 |
Hover a set, a branch or an edge of the tree, or a row, to light what it holds on the drawing; select it and the drawing becomes that tree. A branch is every set beneath it, an edge the part a route choice commits to. The table shows the selected sets; select again, or press Escape, to come back.
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 $σ_1(n)=σ(n)$, the sum of divisors function, and $σ_k(n) = σ(σ_{k-1}(n))$. Is it true that, for every $m, n ≥ 2$, there exist some $i, j$ such that $σ_i(m) = σ_j(n)$?
Sources and licences (D-10):
- https://github.com/google-deepmind/formal-conjectures/blob/c7f31d5fd3d2ca3d69979f2d213eb9b58fe956ae/FormalConjectures/ErdosProblems/412.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-412/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:412, 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-04-26, last changed 2026-07-16, 15 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).