It's only in recent years that it's become trendy for distros to disable unprivileged user namespaces in the name of reducing kernel attack surface. So while a privileged daemon is needed for those distros, there is no such inherent restirction on the kernel level.

[0] https://man7.org/linux/man-pages/man7/user_namespaces.7.html

I expect that there is some relatively easy-to-state solution to this problem, but that it's different in form from what most existing proofs and tools yield. Perhaps if I dumped millions of dollars into it an agent might chance on the solution. Or perhaps my luck is such that my fun little problem is truly intractable...

It's definitely quite curious that the AI labs are able to push these results through seemingly with pure brute force. Perhaps it's largely a function of how many monkeys you have attempting various constructions on top of the known results and strategies the models have memorized.

The length of an expression when written out can definitely be deceiving when pipelining is added to the mix.

In this case, we have the much simpler equational theory of positive integers under addition, multiplication, and exponentiation, which does not include any quantifiers. In fact, Gurevič showed that this theory is decidable [0]. On the other hand, Gurevič later showed that this theory is not finitely axiomatizable [1], so an infinite (but still computable) set of axioms is needed to fully characterize the theory.

[0] R. Gurevič, Equational theory of positive numbers with exponentiation, 1985, https://doi.org/10.2307/2044966

[1] R. Gurevič, Equational theory of positive numbers with exponentiation is not finitely axiomatizable, 1990, https://doi.org/10.1016/0168-0072(90)90049-8

(One of my recent projects has been trying to prove the existence of a 2-colorable subgraph for a certain class of infinite graphs in ZF, which has led me surprisingly deep into choice principles and models refuting them.)

[0] https://mathoverflow.net/a/453944

I somehow doubt that a standard concept you can look up [0] is vacuous due to simple word games.

[0] https://ncatlab.org/nlab/show/torsor

That is to say, the Swiss-cheese approach definitely lends authority, but individual implementations are unfortunately not as foolproof as they're made out to be.

[0] https://github.com/david-a-wheeler/mmverify.py/issues/30

[1] https://github.com/LegionMammal978/mm-verifier-tests/blob/ma...

Now, personally, when I file a bug report for a FOSS project I like to suggest an underlying cause and fix if I can figure it out, but I more rarely just submit a PR outright.

To actually get independence, we need very rigid statements that don't allow any simple way to fudge a solution or counterexample. If anything, statements that mathematicians (and programmers) care about are biased toward undecidability, simply because they're extremely biased toward nontriviality. We put in the hard work of building towers of rigid definitions to that effect.

[0] https://binary.golf/5/

(And NaN payloads in general are a mess across platforms and ABIs, but that can be solved by treating all NaNs as identical.)

[0] https://github.com/rust-lang/rust/issues/114479

The main caveat is that on x86 targets without SSE2, LLVM is deeply wired to use the x87 instructions without attempting to emulate the IEEE overflow/underflow behavior [1]. So perhaps it could be possible to exhibit a discrepancy, but only by compiling for i586 and an ancient target-cpu. It's very doubtful that this was the cause of the original client vs. server issue in TFA's introduction.

[0] https://rust-lang.github.io/rfcs/3514-float-semantics.html

[1] https://github.com/rust-lang/rust/issues/114479

(Meanwhile, I wonder why it's a fair bit harder to look up Ozaki et al.'s optimized version [0] compared to Shewchuk's original paper [1], unless perhaps later authors have found it to be no improvement at all.)

[0] https://www.tuhh.de/ti3/paper/rump/OzBueOgOiRu15.pdf

[1] https://people.eecs.berkeley.edu/~jrs/papers/robust-predicat...

1. The matrix implied by the reference primaries in Table 1: [X; Y; Z] = [506752/1228815, 87098/409605, 7918/409605; 87881/245763, 175762/245763, 87881/737289; 12673/70218, 12673/175545, 1001167/1053270]*[R; G; B].

2. The matrix in section 5.2: [X; Y; Z] = [1031/2500, 447/1250, 361/2000; 1063/5000, 447/625, 361/5000; 193/10000, 149/1250, 1901/2000]*[R; G; B].

3. The inverse of the matrix in section 5.3: [X; Y; Z] = [248898325000/603542646087, 71938950000/201180882029, 36311670000/201180882029; 128304856250/603542646087, 143878592500/201180882029, 14525360000/201180882029; 11646692500/603542646087, 23977515000/201180882029, 191221850000/201180882029]*[R; G; B].

The distinction starts to matter for 16-bit color. The CSS people seem to take the position that the matrix implied by primaries is the true version, but meanwhile, the same document's Annex F (in Amd. 1) seems to suggest that the 5.2 matrix is the true version, and that the 5.3 matrix should be rederived to the increased precision. There's no easy way to decide, as far as I can tell.

Meanwhile, I agree with the author that the ICC's black-point finagling in their published profiles has not helped with the confusion over what exactly sRGB colors are supposed to map to.