Are the solutions on this site actually valid against their standard verifiers? Each was checked
two independent ways: in WASM (the same engines the site runs in your browser —
jsCoq for Coq, lean4.js for Lean) and on GitHub Actions (real Coq, real Lean, real Mathlib).
Snapshot: commit eefcb16, 2026-07-14.
One genuinely open problem here now has a machine-checked solution:
the Google DeepMind Formal Conjectures theorem A317940_f_nonnegative, an OEIS
open question. Here is the full, checkable evidence chain — anyone can reproduce each link and hash.
Scope, stated plainly: this is the only open problem with a verified proof. Goldbach, P vs NP, Riemann, Collatz and every other Open problem on the site remain unsolved — nothing here claims otherwise.
:= by sorry (i.e. left unproved).sorry/admit/custom axiom.A005187, A046644, A317940_f) — byte-identical after stripping comments:
4658ee69…280ef0205dff4de1…f6f0eec ← identicalproofs/lean/A317940/A317940.lean sha256 dbe610e3…dfd1402spec_integrity.json.)sorryAx.The single most direct check. DeepMind's file states the theorem with := by sorry — Lean's explicit
marker for an unproved theorem. Ours proves it. Copy-paste either command:
You can also open the two files in a browser and read line 78 vs. our completed proof:
DeepMind's (line 78, sorry) ↗
·
our archived copy of it ↗
·
our proof ↗.
Reproducibility: fetch the upstream file and re-hash; open the CI run and read the axiom line; or run
lake build in proofs/lean/A317940/ yourself.
Caveat: this establishes the formal theorem is proved. Whether the result/argument is
novel vs. the literature is a separate human question (see the prior-art note under the problem's Materials).
The package also contained OEIS A300997
(a cellular-automaton stabilization time). Being scrupulous about credit: this one is
already solved — by Google DeepMind's AlphaProof, not by this project. Their complete
machine-checked Lean proof (1,118 lines, 0 sorry, sha256 ce24e889…091bf47c)
proves ∀ n≥1, a(n+1)=a(n)+1 ∨ a(n+1)=a(n)+2 —
source ↗.
The submission itself flagged its A300997 material as a reconstruction, “not a new priority claim.”
Our verifiable contribution (CI: tests/a300997.mjs): an independent, from-scratch
re-implementation of the automaton reproduces the sequence and the gap lemma for n = 1..600 — 0 violations:
a(1..16) = 0,1,3,4,6,8,10,11,13,15,17,19,21,23,24,26. Finite evidence consistent with DeepMind's
theorem — not a substitute for it. So: A317940 = a proof we verified; A300997 = a proof we
corroborated and correctly attribute to DeepMind.
A300997 is kept, credited, under /math/archive/ — out of the main catalog so
nothing is misattributed. Our own verified result, A317940, has its full project site at
/math/a317940/.
Standard: the Coq kernel (jsCoq 0.17.1 — Coq compiled to WebAssembly).
Method A: proofs/coq/verify.mjs via jsCoq CLI. Method B:
verify-coq CI run ↗ (success).
| Theorem | Statement | WASM (jsCoq) | Actions (CI) | Verdict |
|---|---|---|---|---|
| gauss_sum | 2·(1+…+n) = n(n+1) | ✔ compiles | ✔ pass | VALID |
| add_comm | n + m = m + n | ✔ compiles | ✔ pass | VALID |
| even_plus_even | even + even is even | ✔ compiles | ✔ pass | VALID |
| mul_one_r | n · 1 = n | ✔ compiles | ✔ pass | VALID |
Soundness spot-check: the same jsCoq kernel rejects a deliberately false proof
(∀ n, n + 1 = n → [Error] Unable to unify "n" with "n + 1"), and the CI driver exits non-zero
on it — so a green result is meaningful, not vacuous. It also caught a real bug: the earlier
gauss_sum proof (simpl; rewrite …; ring) did not compile; it was fixed to
simpl sum_to. nia.
Standard: the Lean 4 kernel (no Mathlib). Method A: the in-browser Lean
(lean4.js / WebAssembly). Method B:
verify-lean CI, job lean-core ↗ (success).
| Theorem | Statement | WASM (lean4.js) | Actions (CI) | Verdict |
|---|---|---|---|---|
| add_comm' | n + m = m + n | ✔ exit 0 | ✔ pass | VALID |
| mul_one_r | n · 1 = n | ✔ exit 0 | ✔ pass | VALID |
| two_add_two | 2 + 2 = 4 | ✔ exit 0 | ✔ pass | VALID |
| even_plus_even | even + even is even | ✔ exit 0 | ✔ pass | VALID |
Soundness spot-check: the in-browser Lean returns exit 0 for these, 4 for
#eval 2 + 2, and rejects theorem bad : 1 = 2 := rfl (exit 1). Each browser run
elaborates in ~110 s; crossOriginIsolated = true.
Standard: the Lean 4 kernel with real Mathlib. WASM: not applicable — the
in-browser Lean ships only the standard library, and Mathlib (GBs of compiled artifacts) cannot be loaded in a
browser. Method:
verify-lean CI, job lean-a317940 ↗ (success).
| Theorem | Statement | WASM | Actions (CI, Mathlib) | Verdict |
|---|---|---|---|---|
| A317940_f_nonnegative | f(n) ≥ 0 for all n ≥ 1, where f∗f = A046644 (the DeepMind open conjecture) | n/a — needs Mathlib | ✔ compiled | VALID |
The CI job fetched 7,869 Mathlib olean files and elaborated the 659-line proof.
The axiom footprint is exactly the three standard Mathlib axioms — no sorryAx, no
custom axiom. The Lean definitions and the theorem statement are byte-identical to DeepMind's upstream spec.
Caveat: this establishes the formal theorem is proved; novelty/priority vs. prior
literature is a separate, human question (see the prior-art note on the problem page).
Standard: exhaustive / exact computation (no floating point). Method A: node tests/run.mjs.
Method B: verify-solvers CI ↗ (success).
| Engine | What "valid" means | Result | Verdict |
|---|---|---|---|
| Propositional logic | tautology decided by the full truth table (De Morgan, Peirce, contraposition, modus ponens…) | ✔ all pass | VALID |
| Number theory | exact BigInt + deterministic Miller–Rabin (Goldbach, Collatz, twins, Mersenne, SAT) | ✔ all pass | VALID |
| A317940 rational | exact rationals reproduce OEIS anchors a(1..4)=1,1,1,7; f(n) > 0 for all n ≤ 20000 | ✔ all pass | VALID |
Reproduce: npm i jscoq@0.17.1 && node proofs/coq/verify.mjs (Coq) ·
node tests/run.mjs (solvers) · push to run all three verify-*.yml workflows
(Lean/Mathlib runs on GitHub's runners).
The three standards used: Coq kernel, Lean 4 kernel (± Mathlib), and exact computation. Every solution shown on the site is VALID against its standard.