submission
Green's open problem 44
Lean accepted this proof on 8 Sept 2026. What happens to it next is decided by people, and that decision is recorded below.
Review decision
Already formalized elsewherePRIOR_EXTERNAL_FORMALIZATION
Rejected under policy v2: PRIOR_EXTERNAL_FORMALIZATION. Green 44 was already solved and formally established before this submission was accepted on 8 September 2026 at 08:29:15 UTC. The earlier public Lean proof is [Erdos1202.erdos_1202_counterexample](https://github.com/plby/lean-proofs/blob/1268917deaaaa0d674f651287027baa26cea9920/src/latest/ErdosProblems/Erdos1202.lean#L412). Its [public proof record](https://github.com/plby/lean-proofs/blob/1268917deaaaa0d674f651287027baa26cea9920/ErdosProblems/Erdos1202.md) was [added on 22 August 2026](https://github.com/plby/lean-proofs/commit/47ad4faf0c3f4f7499ab864dc9bfed3329b54ab0), before acceptance. [Erdos Problems #1202](https://www.erdosproblems.com/1202) identifies the corresponding problem and prior negative resolution. The earlier theorem implies the exact Green 44 reward target: take 1,001 primes and discard the smallest, leaving 1,000 odd primes; the removed-class counts then agree, the survivor count cannot decrease, and the prime-size bound gives the required integer power inequality. The unchanged public proof, its dependencies, and this implication were independently compiled and kernel-checked in Lean 4.33.1, with only propext, Classical.choice, and Quot.sound. The public artifact declares Lean/Mathlib 4.33.0; that original environment was not recreated.
Rejected · decided 9 Sept 2026
Formal statement
True ↔
∀ (N : ℕ) (p : Fin 1000 → ℕ) (A : (i : Fin 1000) → Finset (ZMod (p i))),
have remaining := {x ∈ Finset.Icc 1 N | ∀ (i : Fin 1000), ↑x ∉ A i};
(∀ (i : Fin 1000), Nat.Prime (p i)) →
StrictMono p → p 999 ^ 10 < N ^ 9 → (∀ (i : Fin 1000), (A i).card = p i / 2) → 10 * remaining.card ≤ NVerification report
Every box below had to hold before the proof counted. They are grouped in the order the verifier reaches them.
The task it was checked against
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.
The submission and the sandbox
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.
The trusted build
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.
The kernel's verdict
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
- Bounty.target
Stage COMPLETED · Axioms permitted: propext, Quot.sound, Classical.choice