Erdős problem 859

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.