The math lane: four results, two of them negative

Kairos Signal is a DePIN data business. Alongside it we keep a small research lane in formal methods and number theory. People occasionally ask whether that lane is real or decorative, so here is the ledger, including the parts that did not work.

The rule we hold ourselves to is the same one we apply to network telemetry: **a claim carries a proof or a machine-checkable certificate, or it does not get published.** Two of the four results below are negative. They are here because leaving them out would make the other two less trustworthy, not more.

---

1. Erdős #776 — correct, and second

We derived three parameter cases of Erdős problem #776:

n₀(5) = 14, n₀(6) = 16, n₀(11) = 27, with the exact boundary values **g(14,5) = 10, g(16,6) = 12, g(27,11) = 23**.

The method was a cascade Kruskal–Katona profile criterion with colex constructions, plus He–Tang Proposition 4.1 for the infinite tail. The three cases compile in Lean 4 as corollaries of the published endpoint theorem, with the exact boundary values supplied by explicit witnesses and a proved soundness lemma. No sorry.

They are not new. They are special cases of the complete determination n₀(r) = 2r+4 for 4 ≤ r ≤ 10 and n₀(r) = 2r+5 for r ≥ 11, posted as proof claim #78 by M. Thiim on 17 July 2026 with a full Lean 4 formalization. We found that during the literature check after the derivation, and we corrected our own public README when we found it.

What remains genuinely ours is smaller and duller: an independent replication, and an independent build of Thiim's Lean package on our own hardware — 1,064 targets, exit 0, axiom audit reproduced. That is the second external confirmation of that package, seven weeks after the first. Replication is not discovery. It is still worth publishing, because almost nobody does it.

2. Erdős #778 — the biased clique game, verified on our own machine

Erdős #778 asks about a clique-building game. In the (1:2) biased version, Alice claims one free edge of Kₙ per turn and Bob then claims two; at exhaustion Bob wins if his clique number is strictly larger than Alice's, and a tie is an Alice win.

We wrote an independent search and checker from the game definitions — not a re-run of anyone else's engine — and validated it against the known small boards first. It reproduces them exactly: Alice wins n = 2 and n = 3; Bob wins n = 4 and n = 5, and Bob wins n = 6 and n = 7. On K₈ it confirms Bob wins, in 50.7 seconds over 128,311 stored positions.

The soundness argument is short and is what makes the computation a proof rather than a simulation. At an Alice-to-move position with f free edges, Alice has exactly ⌈f/3⌉ claims left. Define

U(R, B, m) = max{ |S| : C(S,2) ∩ B = ∅ and |C(S,2) \ R| ≤ m }

— the largest clique Alice could still build if Bob never interfered again. Whenever ω(B) > U(R, B, ⌈f/3⌉), Bob has already won under every continuation, because his blue clique cannot disappear and Alice cannot match it. That certifies a leaf. Every other stored position supplies a Bob reply to each legal Alice edge, leading to a stored position with strictly fewer free edges; induction on free edges does the rest.

The quantifier structure is what licenses the pruning: the statement is *for every Alice move, there exists a winning Bob reply*. Every Alice choice must be preserved; only one Bob reply per choice needs to be kept. Dropping Bob's other options shrinks the certificate and cannot manufacture a false positive.

Status of n = 9 at the time of writing: our search is still running. We will publish the result and the certificate when it terminates, whichever way it goes, and a failure to find a certificate under a restricted search will be reported as inconclusive — not as an Alice win. We have not established historical priority for any n ≥ 8; the official problem page returns 403 to automated retrieval, and we could not confirm from the accessible literature whether the (1:2) case at these board sizes is already known.

3. Riemann — a laboratory, two measured laws, and no progress

This is the negative result we are most confident about.

We worked the Hankel-moment route: with F(z) = Ξ(√z)/Ξ(0) and pₖ the power sums over squared Ξ-zeros, RH is equivalent to H_N(0) ≻ 0 for every N, which is equivalent to b_n² > 0 for every n in the Jacobi matrix built from the arithmetic moments — ζ-derivatives at 1/2, with no zeros assumed.

What we actually established, in floating point at 320 digits, not as interval certificates:

monic orthogonal polynomial of the arithmetic moments has 24 real roots, and 1/√root reproduces t₁ and t₂ to 40 digits, t₃ to 38.6, and so on down to t₁₂ to 3.5. This is not new evidence — real-rootedness is the same certificate as pivot positivity — but it is a far more informative object than a determinant. digits ≈ −2.97 + 2.44·log₁₀K − 0.137·(N−1). So the inequality at order N has margin ~10^(−7.5N) while relative tail sensitivity grows like 1.37^N. **Finite zero data cannot certify it uniformly in N.** Any proof along this route must control the zero-counting tail with relative precision shrinking geometrically in N.

That last line is the useful output. It is a constraint on what a proof would have to look like, and it rules out the approach a lot of people try first.

We also moved the basepoint to x = −R with R > 1/4, where every moment becomes an absolutely convergent prime sum plus elementary terms, with no analytic continuation and no zeros — verified at R = 25 against three independent routes (ζ-derivatives, prime sums to 10⁷, and 100k Odlyzko zeros with a density tail) agreeing to 1e−10…1e−16.

One small formal artifact came out of it: RHMetamath.lean, seven theorems, compiling in core Lean 4 with no Mathlib, no sorry and no axiom.

None of this is progress on RH, and we are not going to describe it as such. The remaining statement is unchanged and we write it out exactly each session: for every N, p_{2N+2}(0) − v_N(0)ᵀ H_N(0)^{−1} v_N(0) > 0. Unconditional results identified: none.

4. Our own proof corpus — machine-checking refuted five of our stated properties

We maintain 237 proof obligations about our own pipeline across seven provers — Rocq/Coq, Lean 4, Isabelle/HOL, Dafny, Z3, TLA+ and property-based fuzzing. The artifacts are published, source and compiled, at /proofs. The Isabelle session runs under quick_and_dirty = false, so no sorry is permitted anywhere in it.

On 6 September 2026 we discovered that the ten TLA+ properties had **never actually been model-checked**. No .cfg had been retained, so they were stated, not verified. We fetched TLC, wrote a bounded model, and checked each property alone.

Five of the ten were false as written. QueueBounds failed because the spec increments an acknowledgement counter with no upper guard while two invariants assert it stays bounded. All four liveness properties failed because fairness was declared as weak fairness on the whole next-state relation, which guarantees that something happens, not that any particular enabled action ever runs.

We published that the same day: the corpus page now reads 232 verified, 5 refuted, out of 237 stated. The amended specification ships as a separate v2 file with its own manifest line, because the original file's bytes are pinned by published hashes and editing it in place would invalidate them.

---

Why this is on a DePIN company's blog

The two lanes share one discipline. In the data business the rule is that every published value carries a verify_url pointing at the upstream API, no estimates and no zero-fill; if a metric is not flowing it is absent, not zero. In the research lane the rule is that a claim carries a proof or a machine-checkable certificate.

Both rules mainly cost us things we would otherwise get to say. We were second on #776. The Riemann route produced no progress. Our own corpus turned out to contain five false statements, which we found by checking rather than by asserting, and then published.

That is the whole argument for taking the data seriously: the same people, applying the same rule, in a domain where being wrong is unambiguous.

Artifacts: proof corpus and downloads.