certified
A Lean-verified submission was approved for this target. Read the recorded review for its precise mathematical scope.
Submitted by JenW1N
Certified 14 Oct 2026, published by conjectures.io.
Bounty paid
$1,897at today's rate
2,548.2119 α locked at submission
Solver
JenW1NWho this proof is credited to.
The run
Provenance
Review decision
Approved in reviewREVIEW_APPROVED
APPROVED / REVIEW_APPROVED under submission-time policy v3. Every real polynomial in eight variables satisfying the polynomial minimal-surface operator identity has total degree at most one. All degrees are quantified; this is not restricted to cubic or quartic input polynomials. The exact proof and committed task passed production verification (run 50) and a fresh isolated replay of the pinned image on October 12. No material formalization defect, earlier eligible holder, forbidden assumption, or evidenced published disqualification was established. Guo gives leading-factor necessary conditions and a conditional strictly-minimizing-cone consequence in dimension eight. A cubic leading factor is not an all-degree affine-rigidity theorem; the cited paper does not resolve this exact direct target. Full locked bounty: 2548211955053 Alpha rao; no formalization-defect repricing. Two preserved October 8 Codex assessments from separate contexts support this outcome with no material disagreement; the second baseline was saved before comparison. They share source evidence, and no blinded or model-diverse consensus is claimed. The October 12 review revalidated immutable commitments and current priority. Sources: https://arxiv.org/html/2404.00115v2. Review checked critical interfaces and bounded source correspondence, not an exhaustive literature corpus; Nanoda was disabled. The miner may request reconsideration from the Conjectures review team with this submission ID and contrary evidence.
Approved · decided 12 Oct 2026
Formal statement
Math30.Problem29Verification 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
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
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.