certified
The limiting density of the largest subsets of {1, ..., n} in which no element divides two distinct others exists and is irrational. This result addresses part (ii).
Submitted by JenW1N
The PDF is a working mathematical exposition. Lean verification applies to the formal source, not the prose.
Certified 23 Sept 2026, published by conjectures.io.
Review decision
Approved in reviewREVIEW_APPROVED
Erdős 1062(ii): APPROVED / REVIEW_APPROVED under policy v3. Accepted 2026-09-21 18:55:24.437579 UTC. Production run 38 verified the exact submitted proof and committed task with Lean, Comparator, statement-equality and permitted-axiom checks. The proof establishes both convergence of the native fork-free extremal ratio f(n)/n and irrationality of its limit. No material statement mismatch, earlier eligible submission, or supported disqualification was found. Davis's April 19, 2026 paper establishes existence of the limiting density but explicitly leaves irrationality open; it does not settle this exact target. The full submission-time locked bounty of 3922.148126048 Alpha applies, not a formalization-defect award. Source: https://arxiv.org/html/2604.17613v1 ; original problem: https://www.erdosproblems.com/1062 . The human operator accepted the recorded advisory recommendation. One Codex assessment was completed; multiple independent assessments were not completed and no independent-consensus claim is made. Review relied on recorded production verification, integrity checks, selected proof interfaces and bounded prior-work searches, not a fresh kernel replay or complete line-by-line audit. The submitter may request reconsideration from the review team with contrary evidence, citing submission 8d59a0af-6762-4606-93c9-72dd356a57bc.
Approved · decided 22 Sept 2026
Formal statement
(∃ l, Filter.Tendsto (fun n => ↑(Erdos1062.f n) / ↑n) Filter.atTop (nhds l) ∧ Irrational l) ↔ TrueVerification report
Every box below had to hold before the proof counted. They are grouped in the order the verifier reaches them.
Manifest valid — Passed
The task bundle held together: the exact file set, a strict manifest, and every trusted hash matching the bytes on disk.
Task commitment matches — Passed
The bundle digest the submission committed to is the digest of the bundle that was actually verified.
Production task — Passed
The task came from the production pool rather than a test fixture.
Trusted file hashes match — Passed
The pinned dependencies agree across the manifest, the lockfile and the checkout, down to the same Formal Conjectures commit.
Submission policy respected — Passed
The submitted source passed the static scan: no imports, no axiom declarations, no sorry, no native_decide, no unsafe options.
Production sandbox — Passed
The run happened under real isolation, Landrun with seccomp, and the sandbox passed its own live self-test before the proof was touched.
Challenge built — Passed
The trusted Challenge.lean, which contains no miner code, compiled on its own.
Source type hash matches — Passed
The source theorem in the compiled environment still hashes to the type recorded in the task, so the statement has not drifted upstream.
Solution built — Passed
The submitted Solution.lean compiled.
Statement unchanged — Passed
The theorem the proof establishes has exactly the same canonical type as the task's target - it was not weakened or restated.
Only permitted axioms — Passed
The transitive axiom closure of the proof stays inside the axioms this task permits.
Lean kernel accepted — Passed
The Lean kernel replayed the proof and accepted it.
Nanoda accepted — Not run
A second kernel, written independently of Lean's, also accepted the proof.
One kernel, not two
This task does not require a second, independent kernel, so Nanoda was not run. The verdict rests on a single kernel implementation.
Theorems established
Stage COMPLETED · Axioms permitted: propext, Quot.sound, Classical.choice