JonChesterfield

Pretty torn on this. One the one hand he's not wrong. On the other, it probably means proton are going to leak everyone's email to the world and cease trading shortly afterwards.

Since I'm a customer and don't care _at all_ about any "feature work" that might be being done on email at this point, this isn't great. Leave the damn thing totally alone would seem much better.

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'.

Talking to software engineers about it has a pretty good hit rate for personal anecdotes.

That's the wrong baseline. If you start out oblivious that people are telling you things (with their expression, or with the noises they're making) you get that filter for free. The work is in _not_ filtering out such things. First you have to realise that's a thing (somehow? good luck with the bootstrap), then learn to pay attention, then try to make sense of the result.

Johannes was a leader in his field. LLVM is on a different path with his passing. We are lucky to have worked with him.

Well, git is already distributed, so you could use _any other computer_ instead of gitlab.com...

Customized compiler isn't really a thing in most languages. Because it implies changing the language, and everyone agreeing on what the language is was sort of the point of the whole exercise. Hence all the worries about macros.

SBCL has the right hooks. Jai probably does as well. You could build your own thing on LLVM relatively easily - so Rust _could_ do it if you gave it sufficient access to the compiler, but so could C++ or D.

SIMD bitmasks being ~0 instead of (00000001)+ is common and useful, but there's an annoying language design question in there about what type comparisons between vectors should be (if you don't have a <N x i1> as a type, say because you liked C too much). Shout out to std::vector<bool>.

There is probably interesting work in mojo for this. The library being in MLIR strongly encourages taking that sort of approach. I haven't looked at their implementation though. Happy hacking!

I'm well into the thousands of research papers read. Understood a fair fraction of them. Couldn't tell you what the abstract was for any. The memorable parts are the ideas and the results within the paper.

Some titles stick. "Attention is all you need". "SSA is functional programming". Plus more people see the title than read the abstract. Only one I got to name myself was "Shared Memory Remote Procedure Calls" which I now realise is in exactly the same theme of given the title, you don't need the abstract or the contents.

Turns out that the HN flagging mechanism hides the message from their auth check, so the spam doesn't actually work anyway. Oh well.

Highly recommend qemu instead. The sandbox machines are just more IP addresses on the local network. If you want them completely offline, put them on a network that doesn't have a route to anywhere. The sketchy AI harness is very happy with a whole machine to itself, complete with root access. You can push/pull git repos in from the outside, so all it can do is trash it's own sandbox and get reinstated from scratch by the physical machine below it.

That or X...

This is really important. I am already tired of hoarding rclone copies of huggingface torrents and periodically checking them for bitrot. Pirateface is not a very helpful name for it though and it doesn't seem to have scripted torrent creation either.

Is hosting the same thing at 'academictorrents' actually a viable thing? In terms of peers from either send data to one another?

edit: looks like it can treat huggingface as a backstop for torrents that are otherwise not shared which is interesting, whole load of checksum nonsense I hand rolled disappear if bittorrent handles that. Except it doesn't work?

    Magnet soon No seeders yet - a torrent mints once a seeder packages this model.

So there's some per-torrent work to be done, but I don't know what that is, and I don't see how it can be based on files I have locally _and also_ be an exact match to files on huggingface. So I'm missing something here.

Bastard thing corrupted some of my source code that was "on a shelf". Just gone, no path to retrieving, reimplement it. About a decade ago now and I'm still angry about it. Don't lose the work is table stakes for source control.

You prefer having the harness execute any markdown that looks like it might be a tool call? I had a bad time getting that to work reliably whereas a grammar in the sampler gets it right every time.

I really like the json schemas around the tool calls. Much stricter validation than in codex.

Git might be worth adding to the top level. Currently you've got LSP, grep, glob nicely structured for non-mutating queries across a codebase, but git is behind bash and that means hope or sandboxing.

Thank you for uploading it. Gives a lot of insight into how the deepseek models might expect tool calls to be structured.

Libxml2 segv when the input is large and the transform complicated was something of a surprise to me. Parsing xml is easy enough but I think implementing xslt is going to be a nuisance.