JonChesterfield

Stack overflow started as maximize signal to noise for professionals.

It transitioned to emphasize "less toxic" and in the process minimized signal.

The result has no purpose.

Well, there would be a lot of credible-at-first-glance shite in it, which is rather damaging for an introductory textbook, so there's that.

I'm two chapters in now and if AI wrote this well we'd be much less pissed off about it.

Wonderful.

This construction splits the space into 'small' models with a quadratic lookup cost and 'large' with sub-exponential cost. The small one is by enumerating all SAT problems with their answers, then looking up the answer. The large one is something in polynomials I don't understand. An answer from openai about where the cutoff is was:

    the constructed lookup machine has vastly more states than the estimated total number of physically distinguishable configurations of the observable universe.

I'm not inclined to consider "wrote down all the answers ahead of time, so that's free" as a quadratic time solution to SAT. Nor very convinced by the other half.

So on balance, if this is considered proof that the exponential time hypothesis is false, and openai model reading of the lean was vaguely on point, then I reject the axioms of this system. Not a proof, even if there is lean. I'm OK with being downvoted for that position.

awesome, thanks!

by fucking sorry written at the end of the proof

It's written down in the tokenizer. 256 of the tens or hundreds of thousands of tokens correspond to each byte, done.

Weird paper. Models have had tokens for each byte for ages now. They can read and write individual bytes just fine, in addition to also having multibyte tokens.

A frustration with inference hosting companies is that 'GLM 5.3' is wildly underspecified. What quantization? What numerics? Do you match the official API's probability distribution? Deepseek flash is _all over the shop_ in terms of what people are selling under the name.

> Autoformalization has become a practical reality in 2026

Uh, _maybe_. I've been translating papers into lean for the last week and the correlation between the formalized result and the papers is extremely poor. The cycle seems to be "have a go at the paper, it's a bit hard, prove something different, proclaim success". It's still faster than doing it all by hand but paper in -> lean out in no way ensures a correspondence between the two.

At a minimum we could do it on the same day in the UK as in America. All the meetings moving by an hour four times a year is deeply unhelpful. I have no idea when the clocks change but I definitely missed a lot of meetings by an hour.

You want attribute((overloadable)). Not _Generic. Noone wants _Generic, it should not have been proposed, nor specified, nor implemented.

That works great. The compiler language doesn't matter that much but your language needs a 'runtime' and that is much less annoying to write in C (possibly with bits of assembly, depending on what you're doing) than almost anything else. To a good approximation, your 'compiler' or 'interpreter' amounts to mapping your real language onto a sequence of function calls backed by the 'runtime'.