LegionMammal978
Joined 5 years ago
Karma
3,399
Submissions
1,408
Member since
Feb 20
Recent submissions
Comment · 8 days ago
Comment · 19 days ago
I can't speak for the FFT claim, but least the sub-O(n log n) multiplication claim is for the multitape Turing machine model with a fixed number of tapes, which if anything is more restrictive than actual random-access memory. Of course, it's still galactic just like the O(n log n) algorithm, but it definitely seems like there's something there.
Comment · 1 month ago
https://mathoverflow.net/q/511601 is a fun little math problem that came up in one of my projects, I didn't have any reason to expect it to be particularly tough, but none of the models I've thrown at it have been able to solve it past a few minor reductions and special cases.
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...
Comment · 1 month 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 standard tools, but the LLMs do not recognize it as a major open problem they should give up on. So they seriously try it, but typically end up in a loop of inventing certain classes of simple solution or counterexample attempts, defeating them, and trumpeting each one as a major result, each time inventing some new terminology.
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.
Comment · 1 month 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 very large degrees can be calculated in the same time as a single correctly-rounded sqrt, especially when fma is available. Seemingly, the only real cost is the added register pressure.
The length of an expression when written out can definitely be deceiving when pipelining is added to the mix.
Comment · 2 months 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 extending the signature or using some method of description other than a set of axioms.
Comment · 2 months 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 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
Comment · 2 months 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 well-founded relation, "no infinite descending chains" doesn't imply "every nonempty subset has a minimal element" without dependent choice.
(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.)
Comment · 2 months 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".
Comment · 3 months 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 standard concept you can look up [0] is vacuous due to simple word games.
Comment · 3 months 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 from mmverify.py. A sound verifier isn't too difficult to write in terms of architecture (I just wrote one myself for differential testing [1]), but it requires some close attention to the details.
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...
Comment · 4 months 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 niche libraries to observe how their behavior has changed. But for most traditional distribution methods (putting the tarball up on your website or on a SourceForge-style website), the common assumption is that no one wants old broken versions, so you can regularly wipe everything but the last 1-3 versions to reduce clutter: the consequence is that the old versions accidentally saved on archive.org may be the only copies left anywhere. The more recent practice of publishing Git repos has considerably improved this situation.
Comment · 4 months 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 determining whether a project is receptive at all, then whether it has a reasonable number of hoops for outsiders to jump through.
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.
Comment · 5 months 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 fragments. In fact, for every slightly nontrivial statement that requires actually building a construction, there are billions more that can be instantly solved via a few simplifications, and statically pruning the search tree a bit is the best we can do.
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.
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