Viewing profile — LegionMammal978

One curiosity that in the case of infinite graphs, "no odd cycles" doesn't imply "2-colorable" without the axiom of choice for families of 2-element sets [0]. It's somewhat similar…

"The set is not collinear" here means "there is no straight line passing through all the points simultaneously", not "there is no straight line passing through some three points".

> Corollary 14 (There is no such thing as a torsor). A torsor is defined as a “group without a distinguished identity element.” No such object exists. The proof is immediate from t…

As it happens, the Python verifier mmverify.py has an even simpler soundness bug [0], and so far I've reviewed two independent AI-written verifiers that have replicated that bug, s…

The problem is, some information is interesting only to a tiny audience long after the fact, so there's no chance anyone would've thought to curate it in the moment. E.g., for a fe…

On the other hand, there's been an endless parade of recent posts from other FOSS maintainers saying "we don't want your drive-by PRs": it's not hard to see people getting dissuade…

To be fair, in the most literal sense, the vast majority of syntactically-valid statements in a typical FOL encoding will be trivial. One of my side-projects has been trying to fin…

I always thought of it as analogous to the silent Ls in would / should / could , calf , half , chalk , caulk , and Polk .

I did actually make an attempt at that once for BGGP5 [0]. (That is, making a minimal, horribly insecure 'client' implementing just enough behavior to get a response from a server.…

Alas, compilers have historically fudged the behavior on some 32-bit targets, e.g., x86 targets without SSE2 [0], so you'd have to go all the way to soft-float implementations if y…

At least the Rust compiler (TFA's project is written in Rust) tries to configure LLVM specifically to avoid these discrepancies, and to treat all basic floating-point operations ex…

Yeah, in general, this is a problem that people have spent a lot of time thinking about; while floating-point numbers can be finicky, they're what you have to work with if you have…

sRGB has bugged me from the start, since it's not even clear to me which actual matrix to use to convert between linear sRGB colors and XYZ colors. I count at least 3 different mat…

You can pick a uniform random orientation without trig functions by first generating a random point in the unit disk via rejection sampling, then projecting it onto the boundary [0…

> But what about the range? While it’s true that you get twice the range, surprisingly often the code in the range above signed-int max is quite bug-ridden. Any code doing somethin…

> However, an axiom of infinity is independent, it doesn’t contradict anything in standard formalizations, and so it doesn’t make sense to say “infinity is wrong”. Suppose we start…

> The implicit update surface is somewhat limited by the fact that versions in Cargo.toml implicitly assume the `^` operator on versions that don't specify a different operator, so…

Traditionally in x86, only the first byte is the opcode used to select the instruction, and any further bytes contain only operands. Thus, since there exist 256 possible values for…

Try 81 bytes for an x86-64 executable, or 77 bytes for the same if you run it on a VM with 5-level paging: https://tmpout.sh/3/22.html

Even in a NAT-less world, the common advice is to use a firewall rule that disallows incoming connections by default. (And I'd certainly be worried if typical home routers were con…

> The LLM can a priori test on all possible software and hardware environments, test all possible edge cases for deployment, get feedback from millions of eyes on the project expli…

> But the users would have to maintain their own forks then. I suppose the idea would be, they don't have to maintain it: if it ever starts to rot from whatever environmental chang…

Just looking at the formula in the code (and the book it came from), we see that the approximation is of form arcsin(x) = π/2 - P(x)*sqrt(1-x). It is called a minimax solution in b…