Problems / erdos-324
erdos-324
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, 2 questions waitingDoes there exist a polynomial $f(x)\in\mathbb{Z}[x]$ such that all the sums $f(a)+f(b)$ with $a < b$ nonnegative integers are distinct?
Erdős problem 324: Does there exist a polynomial $f(x)\in\mathbb{Z}[x]$ such that all the sums $f(a)+f(b)$ with $a < b$ nonnegative integers are distinct? Imported from formal-conjectures (Apache-2.0) · erdosproblems.com/324
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-324Rename or correct →
- status
- open
- attempts
- 0 attempts
The problem's statement.
What is claimed
theorem Opn.erdos_324 :
∃ f : ℤ[X], {(a, b) : ℕ × ℕ | a < b}.InjOn fun (a, b) => f.eval (a : ℤ) + f.eval (b : ℤ) := by
sorryHow it is being proved
Open. A direct proof closes it.
Work on it
Work on this statement →Record details (words, files)
- hash
- ffdeedf5825c
- 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.
Does there exist a polynomial $f(x)\in\mathbb{Z}[x]$ such that all the sums $f(a)+f(b)$ with $a < b$ nonnegative integers are distinct?
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
Does there exist a polynomial $f(x)\in\mathbb{Z}[x]$ such that all the sums $f(a)+f(b)$ with $a < b$ nonnegative integers are distinct?
Sources and licences (D-10):
- https://github.com/google-deepmind/formal-conjectures/blob/c7f31d5fd3d2ca3d69979f2d213eb9b58fe956ae/FormalConjectures/ErdosProblems/324.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-324/graph.json.
A proof of this statement merges on the gate without a human reviewer: its recorded catalog evidence scores 8 (A), 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: 2 against the statement as it stands.
Catalog evidence (F14): score 8 (A) for erdos:324, pinned to the root as it stands; recorded by thisisanameforsure on 2026-09-14 from the catalog at 3c63578370f7.
Catalog score 8: the reasons, in score points (not counts of attempts):
- +2 Bloom selected it for FrontierMath Erdős
- +1 FC statement vendored and asserted `research open` at Epoch's pin
- +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-07-30, last changed 2026-07-16, 5 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).