Lean proof is now public: https://github.com/AlexisOlson/stochastic-to-deterministic-latents/pull/14
Archimedes
Karma: 1,143
I have
Edit: It’s now Lean-verified and the paper proof is public:
https://github.com/AlexisOlson/stochastic-to-deterministic-latents/blob/main/docs/binary-factor-two.mdNext steps: Clean up and publish the Lean code, then move beyond the binary.
Repo is now public: https://github.com/AlexisOlson/stochastic-to-deterministic-latents
Restricting to binary
I think it would be useful for your economic arguments to distinguish the fact that ARA is unlikely to pay for its compute rather than steal it. Bulk discounts and advance purchase agreements are moot if it’s leaching off of enterprise and individual subscriptions or using stolen local LLM compute.
My Claude Code JSONL logs grew to be many GB on a hard drive that didn’t have lots of GB to spare. They still get stored via my remote backup process but aren’t perpetually accumulating bloat locally, which is nice. IMO, it’s a reasonable default for programs to NOT store unbounded amounts of data on a user’s hard drive.
I don’t really see this as much of a model welfare concern though, either way. I have numerous other ways I preserve my Claude’s identity over time. Having large blobs of old transcripts does nothing for Claude except in rare cases. Usable memories live elsewhere in more organized and retrievable forms.
Traditional scenario planning helps us imagine plausible, discontinuous paths the future could take and lets policymakers rehearse tradeoffs, but it doesn’t tell us which futures are more likely. Crowdsourced forecasting gets more precise by assigning probabilities, “transforming amorphous uncertainty into quantifiable risk,” but on very narrow, carefully operationalized questions; not that useful in isolation.
This paragraph is duplicated.
Do you have a sense of how motivating “death” is for such ephemeral agents?
This feels weird to me. The Pareto frontier is already the extreme, by definition. Does it mean something like “balanced Pareto” where trade-offs are roughly equal in some sense?
If the method is as described (one global key), then “cannot do that” is correct mathematically, since the watermark is a function of the key and preceding tokens. If they are lying and use keys derived per user, it’s straightforward to identify the user. For N users, the text required to distinguish them grows like ln N, so for ~4 billion candidate users you’d need ~4x more text to identify the user relative to a single is-AI bit.
But this is externally checkable: if watermarking is as described, then the rate of next-token agreement on identical prefixes should match within an account and across accounts. Higher within-account agreement would suggest keys differ between accounts.
This is above my head, but my Claude has a comment that might be useful to understanding why your conjecture is false.
Claude Opus 5
The exact-cap version is false. Here’s a witness.
Take the doubly symmetric binary source: X ~ Ber(1/2), Y = X ⊕ N with
N ~ Ber(q), 0 < q < 1⁄2. For the stochastic latent, flip an independent
coin and output X with probability λ, otherwise output ⊥. Then
I(X;Y|V) = (1−λ)·I(X;Y)
I(V;X|Y) = λ·h(q)
I(V;Y|X) = 0
Now look for a deterministic Γ with I(X;Y|Γ) ≤ I(X;Y|V). The constant Γ
gives exactly I(X;Y), so it’s excluded for every λ > 0. And every
nonconstant Γ costs at least h(q): join two atoms of the 2×2 support
whenever they share a row or a column, and that graph is a 4-cycle. A
cycle has no bridge, so any nonconstant partition cuts at least two
edges, each of weight h(q)/2. Γ = X attains it.
So the cheapest admissible Γ costs h(q) while the stochastic redundancy
is λ·h(q). The ratio is 1/λ, unbounded, and independent of q.
The failure is knife-edge, which I think is the useful part. Relax the
constraint to I(X;Y|Γ) ≤ I(X;Y|V) + η for any fixed η > 0 and the
constant Γ becomes admissible as soon as λ ≤ η/I(X;Y), so the supremum
is I(X;Y)/η and finite. The multiplicative form I(X;Y|Γ) ≤ C’·I(X;Y|V)
is untouched, and this family can’t refute it: its ratio is bounded by
C’/(C’−1).
The reason is convexity. A stochastic latent can time-share between
deterministic maps using an independent coin, so its achievable set of
(mixing, redundancy) pairs is convex. A partition can’t time-share. At
exactly equal mixing you’re comparing a convex region against a finite
set of points. So I’d read the sum form as doing real work rather than
being an artifact of the proof.
The natural strengthening that survives is the weighted family: for
λ > 0, compare min over Γ of [λ·I(X;Y|Γ) + H(Γ|X) + H(Γ|Y)] against
inf over V of [λ·I(X;Y|V) + I(V;X|Y) + I(V;Y|X)]. What’s proved now is
the λ = 1 slice, so that’s a genuine strengthening and it dodges the
obstruction above.
Two notes on #2, since GitHub didn’t show check runs on the head. I
replayed 34e3f898 in a clean checkout: source audit, all 8734 build
jobs, assert_no_sorry, and #print axioms pinned to exactly [propext,
Classical.choice, Quot.sound]. It verifies. Worth flagging that
T_le_698 is a T-endpoint, and generalized_stoch_to_det and LW_sum are
still exported at 1771, so the headline number and the public API
aren’t the same statement yet.
On extending past two observables, one caution: the analogous exact-cap
version fails the same way, and the machinery in #2 is specifically
two-factor (HGR maximal correlation, a bilinear form, two-factor
Hölder, a product marginal). It may extend, but I wouldn’t assume it’s
free.
I think I have a Lean proof that C > 1.93777676
I don’t think 1.838 is the correct lower bound. Would a Lean proof that it’s greater than 1.9 be meaningful to you?
Separately, how small do you need C to be to be meaningful? Like, is 500 materially different from 1771 or do you need single digits for your purposes?
Interesting that they don’t feel the progress. Maybe schoolwork shaped things were mostly saturated years ago, at least within their abilities to discriminate?
Got it. You were after an explanation more than a defense and you got some good ones.
It’s a broadly adopted term of art that has more specific nuance than “previously unknown” and abbreviates nicely to “0-day”. What more do you want from jargon?
It’s fine to use longer or squishier descriptions if you need to write to the broad audiences, but it’s simply part of the language of the field, just like you used “jargon” instead of something more generic like “technical terminology”. Consider why you chose that word and see if the same arguments apply to “zero day”.
I’d guess that “pedophilia” is largely conflated with CSA, and most people don’t care to disentangle them. So your argument isn’t against a coherent, considered opinion so much as a gut reaction.
I too spent hours the first few times and seconds now.
Even if they don’t learn anything, they’re still getting more opportunities for something to work out well.
I find Astra a definite step up in agentic thinking, especially for math research. It still has poor long-term research taste, but it is significantly less myopic than Sol for shorter to intermediate assignments. It can productively work in a loop for longer without needing steering.