LegionMammal978

4 ms·

1.
by LegionMammal978 24d ago
Yeah, that mirrors what I've seen throwing some of the leading models at a set-theory problem that's stumped me ( https://mathoverflow.net/q/511601 ): in this case, the problem does not easily yield to the stan
2.
by LegionMammal978 26d ago
Yeah, I just recently learned about Estrin's method when fooling around with some polynomial approximations. I'd been scaling the output by a sqrt term to get better accuracy at small degrees, but it turned out that polynomials of
3.
by LegionMammal978 2mo ago
Not using a set of axioms written in the original signature, of equations using the three operations and the constant 1. It's certainly possible to come up with a finite description of the true sentences in the theory, but only by exte
4.
by LegionMammal978 2mo ago
No, Gödel's incompleteness theorem applies to theories that can interpret first-order arithmetic, which includes quantified statements like "for all x , there exists a prime p > x ". In this case, we have the much simp
5.
by LegionMammal978 2mo ago
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 to how in the definition of a
6.
by LegionMammal978 2mo ago
"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".
7.
by LegionMammal978 2mo ago
> 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 the axioms of group theory. I somehow doubt that a standar
8.
by LegionMammal978 2mo ago
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, since they apparently really like to copy the strategy f
9.
by LegionMammal978 3mo ago
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 few of my projects I like to dig up old versions of
10.
by LegionMammal978 4mo ago
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 dissuaded from the whole dance of determini
11.
by LegionMammal978 5mo ago
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 find the shortest statements independent of ZF and some of its
12.
by LegionMammal978 5mo ago
I always thought of it as analogous to the silent Ls in would / should / could , calf , half , chalk , caulk , and Polk .
13.
by LegionMammal978 5mo ago
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.) But I got demoralized by how much space the bina
14.
by LegionMammal978 5mo ago
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 you really want guarantees. But these targets are rare,
15.
by LegionMammal978 5mo ago
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 exactly as written with round-to-nearest behavior [0]. It
16.
by LegionMammal978 5mo ago
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 inputs at multiple scales. (Meanwhile, I wonder why it
17.
by LegionMammal978 5mo ago
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 matrices in IEC 61966-2-1, each of which I have seen diffe
18.
by LegionMammal978 5mo ago
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]. Of course, using rejection sampling for disk points will
19.
by LegionMammal978 5mo ago
> 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 something like (2U * index) / 2U in this range will have qui
20.
by LegionMammal978 5mo ago
> 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 with ZFC - Infinity as our base system. Then the negatio
21.
by LegionMammal978 6mo ago
> 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 "1.2.3" means "1.2.x, where x >
22.
by LegionMammal978 6mo ago
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 the initial byte, there are at most 256 possible opcodes to
23.
by LegionMammal978 6mo ago
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
24.
by LegionMammal978 6mo ago
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 configured otherwise.) So either way, you'd need the
25.
by LegionMammal978 6mo ago
> 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 explicitly or implicitly via bug reports and usage, find good
26.
by LegionMammal978 6mo ago
> 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 changes, then they can just get the LLM to patch it, or
27.
by LegionMammal978 7mo ago
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 both, and the simplest form of minimax optimization is f
28.
by LegionMammal978 7mo ago
Actually, we can improve this a bit further, by also adjusting the "π/2" constant in arcsin(x) = π/2 - P(x)*sqrt(1-x). We take coefficients [1.5707256467180715, -0.21298179775496026, 0.07727939759417458, -0.0213210284991
29.
by LegionMammal978 7mo ago
The coefficients given are indeed a near-optimal cubic minimax approximation for (π/2 - arcsin(x))/sqrt(1-x) on [0,1]. But those coefficients aren't actually optimal for approximating arcsin(x) itself. For reference, the coef
30.
by LegionMammal978 7mo ago
Even for boolean logic problems, a minimum-size CNF or DNF will not necessarily be the cheapest solution in terms of gates. As far as I know, hardly anyone has even attempted automatic minimization in terms of general binary operators.

More ›