Is there any pre-existing proof of A317940_f_nonnegative? This page searches deep,
reproducibly, and honestly — because the one thing still under review for our submission is novelty.
Fetches DeepMind's actual conjecture file right now and checks whether the theorem is still stated with
sorry (Lean's marker for “unproved”). If it ever stops being sorry, someone proved it upstream.
Searched all of GitHub's indexed code (via the code-search API). No existing A317940 proof — notably, DeepMind's AlphaProof published a proof for the neighbouring sequence A300997, but not for A317940.
| Query | Results | |
|---|---|---|
| A317940 org:google-deepmind | 0 | clear |
| A317940_f_nonnegative language:lean | 0 | clear |
| A317940 language:lean | 0 | clear |
Reproduce: GitHub code search “A317940 language:lean” ↗ · the exact theorem ↗.
The deep CI crawl (2026-07-15, code + issues API) confirmed this and additionally scanned issues. Its one flag — an issue titled “A317940 verifier console” — was our own CI-status issue (explicitly “not a mathematical claim”), not prior art; the crawler now excludes the submitter's own repositories.
The tools/prior-art/check.mjs crawler runs deep in CI (weekly + on demand:
prior-art workflow ↗)
across GitHub, OEIS and arXiv, and fails loudly if any source turns up a candidate prior proof. Latest committed report:
prior-art-report.json…From PRIOR_ART.md: the binary digit-sum generating-product identity is classical (Schneider & Schneider, 2018). The positivity argument, the Dirichlet-square-root application, and the general fractional-power statement appear to be new — but this is a search result, not an expert judgement. Independent human/literature review is still the deciding step for the “novelty” part of the submission's under-review status.