I still consider the article important, as it demonstrates techniques to conduct searches, and emphasizes the very early stage of the research (establishes non-uniqueness for example), openly wonders which other binary operators exist and which would have more desirable properties, etc.
Sometimes articles are important not for their immediate result, but for the tools and techniques developed to solve (often artificial or constrained) problems. The history of mathematics is filled with mathematicians studying at-the-time-rather-useless-constructions which centuries or millennia later become profound to human interaction. Think of the "value" of Euclid's greatest common divisor algorithm. What starts out as a curiosity with 0 immediate relevance for society, is now routinely used by everyone who enjoys the world wide web without their government or others MitM'ing a webpage.
If the result was the main claimed importance for the article, there would be more emphasis on it than on the methodology used to find and verify candidates, but the emphasis throughout the article is on the methodology.
It is far from obvious that the tricks used would have converged at all. Before this result, a lot of people would have been skeptical that it is even possible to do search candidates this way. While the gradual early-out tightening in verification could speed up the results, many might have argued that the approach to be used doesn't contain an assurance that the false positive rate wouldn't be excessively high (i.e. many would have said "verifying candidates does not ensure finding a solution, reality may turn out that 99.99999999999999999% of candidates turn out not to pass deeper inspection").
It is certainly noteworthy to publish these results as they establish the machinery for automated search of such operations.
The original article explicitly acknowledged this limitation, that while in "the classical differential-algebraic setting, one often works with a broader notion of elementary function, defined relative to a chosen field of constants and allowing algebraic adjunctions, i.e., adjoining roots of polynomial equations," the author works with the less general definition.
Neither the present article, nor the original one has much mathematical originality, though: Odrzywolek's result is immediately obvious, while this blog post is a rehash of Arnold's proof of the unsolvability of the quintic.
Yes, this article is kicking in open doors, the original article was quite clear about the scope.
The present article could rather have spent time arguing why this isn't like NAND gate functional completeness.
I would have thought the differences lie in the other direction: not that trees of EML and 1 can describe too little, but that they can describe too much already. It's decidable whether two NAND circuits implement the same function, I'm pretty sure it's not decidable if two EML trees describe the same function.
> It's decidable whether two NAND circuits implement the same function, I'm pretty sure it's not decidable if two EML trees describe the same function.
Perhaps, perhaps not, same function so basically is this question solvable:
if a user brings EML functions f and g; given their binary EML trees; can we decide if they represent the same function, so the question form is
A(x)=0 EVERYWHERE?
(like given 2 fractions a/b == c/d ? do the fractions represent the same fraction?)
From Wikipedia link reikonomusha gave:
> Miklós Laczkovich removed also the need for π and reduced the use of composition.[5] In particular, given an expression A(x) in the ring generated by the integers, x, sin xn, and sin(x sin xn) (for n ranging over positive integers), both the question of whether A(x) > 0 for some x and whether A(x) = 0 for some x are unsolvable.
Here the question forms are
1) exist x such that A(x) > 0 (does there exist an x where A(x) becomes positive?)
2) exist x such that A(x) = 0 (does there exist a value such that A(x) becomes 0? or basically find real roots
so at least the forms on WikiPedia don't generate the results both of you claim it does.
it does present undecidability results, but not straightforwardly in the context of this EML work.
second the Richardson's theorem is about the function on the reals, not complex functions (I mean the roots must lay somewhere)
> an expression in the ring generated by the integers, x, sin xn, and sin(x sin xn)
We can always write AML trees for expressions generated by the integers, x, sin xn, and sin(x sin xn), right?
So we should be able to write EML trees for any two such expressions, A and B. If they're equal everywhere, then A - B = 0 everywhere. A - B is also in the aforementioned ring.
If there was a decision procedure always to determine if EML trees represent the same function, then that contradicts Miklós Laczkovich's extension, right?
decidability does not distribute over pointwise question asking on sets, or if you believe it does, show us the proof.
Telling if an EML(x,y),1 constructed expression is identically 0 is in the gray zone, as far as I can tell, it has neither been proven decidable nor been proven undecidable.
Nevertheless regardless of decidability the authors clearly show the multipoint sampling/testing is a decent filter, and the shorter resulting expressions have been proven correct in the results for the construction at least.
Arnold (as reported by Goldmakher [1]) does prove the unsolvability of the quintic in finite terms of arithmetic and single-valued continuous functions (which does not include the complex logarithm). TFA's result is stronger, which is something about the solvability of the monodromy groups of all EML-derived functions. So it doesn't seem to be a "rehash", even if their specific counterexample could have been achieved either in fewer steps or with less machinery.
Arnold's proof can be used to show that certain classes of functions are insufficient to express a quintic formula.
These classes can always safely include all single-valued continuous functions (you cannot even write the _quadratic_ formula in terms of arithmetic and single-valued continuous functions!), but also plenty of non-single-valued functions (e.g. the +-sqrt function which appears in the well-known quadratic formula).
Applying Arnold's proof to the class given by arithmetic and all complex nth root functions (also multivalued) gives the usual Abel-Ruffini theorem. But Arnold's proof applies to the class "all elm-expressible functions" without modification.
and its depressing when the rare actual progress is made, a collection of jealous practitioners comes to party-poop all over the place, for bringing the insights that make the result from then on immediately obvious.
This may or may not be true; but the burden of proof should not lay with the reader.
Please provide (in absence of which every reader can draw their own conclusions) a reference which simultaneously:
1) predates Odrzywolek's result
2) and demonstrates the other unary and binary operations typically tacitly assumed can be expressed in terms of a single binary operation and a constant.
(in other news: I can spontaneously levitate, I just don't feel like demonstrating it to you right now...)
Questions which have never been asked or answered before, but to which practitioners have immediately obvious answers, are dime a dozen in mathematics.
You can find thousands of such questions on Math StackExchange. Take e.g. [1]: never been asked anywhere else, interesting enough, yet answered pretty much immediately by two separate mathematicians.
"Is there a single constant and function with connected domain that can express all of $\log, \exp, \sin, \dots$?" would have made a fine question there too, the type that gets a thorough answer very quickly if anyone bothers to ask it.
> the burden of proof should not lay with the reader
You were the one who made the claim that "this is one of the most significant discoveries in years". Feel free to substantiate that claim first, according to the same standards. Are there any authors who ask this question, and/or suggest that they don't know an answer?
> Repeating myself, when we speak of bugs in a verified software system, I think it's fair to consider the entire binary a fair target.
Yes, and that would be relevant if this was a verified software system. But it wasn't: the system consisted of a verified X and unverified Y, and there were issues in the unverified Y.
The article explicitly acknowledges this: "The two bugs that were found both sat outside the boundary of what the proofs cover."
1/ lean-zip is open source so it's much easier to have more Claude's eyes looking at it
2/ I don't think Claude could prove anything substantial about the zip algorithm. That's what lean is for. On the other side, lean could not prove much about what's around the zip algorithm but Claude can be useful there.
MS Flight Simulator w/ VATSIM [1] l has this, in the sense thar you can participate as a pilot or a controller, although you are not assigned these roles at game start.
Anti-griefing works by keeping the barriers to entry very high, so chances are you won't try VATSIM, even though MSFS is technically available on Steam.
The thread started out off the rails. Contrary to the claims of youre-wrong3, garbage collection is not a particularly high paying job and has no real trouble getting new hires.
> When asking people to write code in a language, these restrictions could be onerous. But LLMs don't care, and the less expressivity you trust them with, the better.
But LLMs very much do care. They are measurably worse when writing code in languages with non-standard or non-existent operator precedence. This is not surprising given how they learn programmming.
> I have noticed that only white people commit to living in the UK without becoming citizens.
Alas, you've not discovered a hidden pattern, except maybe a hidden pattern in the kinds of people you socialize with. Chinese nationals cannot hold dual citizenship, and renouncing their Chinese citizenship creates very serious complications, including around property and inheritance when parents die, which you would be aware of if you knew any Chinese person well enough to have had this conversation with them.
Based on gov.uk immigration system statistics data and tables, among those with indefinite leave to remain, the most likely to seek citizenship are British Overseas Citizens, Austrians and Lithuanians. The least likely are Moroccans and Venezuelans.
Weird in the Venezuelans case, as there is no restrictions for double nationality and having only Venezuelan citizenship doesn't have many advantages. I would guess that it is because most Venezuelans living there already have an European passport due to parents/grandparent, so no need/can't get a third
Cannot only if the other European country does not allow dual nationality.
If they are permanently settled in the UK surely it would be better to have British citizenship rather than that of a country they do not live in?
The nationalities listed are all very small groups in the UK. maybe they are not really permanently settled? Someone who moves somewhere for work might end up living there a decade (and in the UK that would mean getting indefinite leave to remain) and then returning.
I admit not knowing a lot of Chinese nationals, but I do know a very wide range of people. Of course, issues with property and inheritance only apply to people who have sufficient for it to be a major issue.
Could you link to the stats showing that? What about all the other countries? What is the position of BNOs?
Indefinite leave to remain is not the same as permanently settled - there is a difference between long term and the rest of your life.
What if you asked your favorite AI agent to produce mathematics at the level of Vladimir Voevodsky, Fields Medal-winning, foundation-shaking work but directed toward something the legendary Nikolaj Bjørner (co-creator of Z3) could actually use?
Well, you'd get this embarrassing mess, apparently.
Some of my favorites:
DoctorOetker: "I'm still reading this, but if this checks out, this is one of the most significant discoveries in years."
cryptonektor: "Given this amazing work, an efficient EML operator HW implementation could revolutionize a bunch of things."
zephen: "This is about continuous math, not ones and zeroes. Assuming peer review proves it out, this is outstanding."
[1] https://news.ycombinator.com/item?id=47746610
[2] https://www.reddit.com/r/math/comments/1sk63n5/all_elementar...
reply