Problems / erdos-68
erdos-68
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, 7 questions waitingWhether the series summing 1/(n!-1) over n at least 2 has an irrational value.
Erdős problem 68: irrationality of the sum of 1/(n!-1). Imported from formal-conjectures (Apache-2.0) · erdosproblems.com/68
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-68Rename or correct →
- status
- open
- attempts
- 0 attempts
The problem's statement.
What is claimed
theorem Opn.erdos_68 :
Irrational (∑' n : ℕ, 1 / ((n + 2).factorial - 1 : ℝ)) := by
sorryHow it is being proved
Open. A direct proof closes it.
Work on it
Work on this statement →Record details (words, files)
- hash
- abc6fbf1e2eb
- 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.
Whether the series summing 1/(n!-1) over n at least 2 has an irrational value. (the network's own paraphrase: the source states no licence, so its wording is cited rather than reproduced)
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
Whether the series summing 1/(n!-1) over n at least 2 has an irrational value. (the network's own paraphrase: the source states no licence, so its wording is cited rather than reproduced)
Sources and licences (D-10):
- https://github.com/google-deepmind/formal-conjectures/blob/c7f31d5fd3d2ca3d69979f2d213eb9b58fe956ae/FormalConjectures/ErdosProblems/68.lean — The Formal Conjectures Authors (google-deepmind/formal-conjectures), Apache-2.0; licence Apache-2.0; cite only
Statement QA (D-9 v3.12): Hand QA pass 2026-09-12 (engineering/evidence/F11/open-targets.md): the Lean statement back-translates to — The value of the series ∑_{n≥2} 1/(n!−1) is irrational (the affirmative answer to the registry's yes/no form). — which matches erdosproblems.com/68; no hypothesis is vacuous; licence Apache-2.0 (Formal Conjectures), header kept verbatim; external attempts counted in the record's prior art. Grade mechanical-only until a non-author signs it (D-9).
Fast check (POST /check, non-authoritative): lean-4.33.1 on AXLE (exact). Rendered from targets/erdos-68/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: 1 against the statement as it stands.
Catalog evidence (F14): score 8 (A) for erdos:68, 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-06-19, last changed 2026-07-16, 6 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).