An interesting problem must have a description that fits in a brain, at least for now. Your description-length argument assumes arbitrarily large storage.
Sorry, I assumed the inductive construction was implied; you can indeed describe properties of that particular interesting problem (though of course you can’t hold its definition in your head), so it goes in the list. Keep going. At some point you’ll hit problems where the process of constructing the problem doesn’t even fit in a brain, etc. There are at least countably many problems, but finitely many problems which any algorithm-which-fits-in-the-brain can describe given finitely many inputs-which-fit-in-the-brain.
This isn’t an enormously important point - the actual question at issue is an empirical one, “in a steady state, can we produce interesting problems at a rate that exceeds our ability to solve them and integrate our understanding” or something like that - but I did rankle at a “trivial” proof which is invalid due to equivocating between multiple definitions of the word “interesting” (which should really take an object, “interesting to me” vs “interesting to something smarter than me”).
I'd be interested in hearing a field report on this! For example, I can easily imagine that they're great at walking through the proof step by step, explaining background as necessary; but as TFA notes, one of the most important questions is "why is this definition the way it is?", and my bet would be that the Lean is not enough to help the LLMs meaningfully in answering that.
LLMs like even the sota flash models have great range of background math knowledge and have no problem reading and understanding flt level of math. On the other hand you don't want to go through 13 million lines of often repetitive code line by line. Models are great at synthesizing math content out of code. My contribution is to steer it through subjects of most interests to me, drill down into jargons that can be confusing, be creative in using computation for illustration (which coding agents can execute very proficiently) etc.
(Apparently I was extremely unclear with this text. For clarity: if you want to actually understand surreal numbers, go and read On Numbers and Games, by Conway, which is a delightful book; or get an LLM to talk you through Wikipedia. Original text follows.)
It’s a terrible explanation. A surreal number is defined as a pair of sets of surreal numbers (where you fiddle around the recursion in that definition by defining them in waves, so strictly speaking you’re defining “the surreal numbers born at time T” for each individual T given access to the surreal numbers born at all earlier times, and then you “take the union across all times”, scare quotes because there are too many times for this to result in a set). Zero is a surreal number but the LLM is using the word “zero” to mean “the set containing just the surreal number 0”; “nothing” here is the LLM’s obtuse word for the empty set. Wikipedia may actually be easier to follow.
LLM didn't write anything in my post; these are all my words and my choices. Conway himself described surreal generation in short like this in ONAG:
> We may say that Cantor was only interested in moving ever rightwards, whereas Dedekind stopped to fill in the gaps, so that R was always empty for Cantor, never empty for Dedekind. It is remarkable that by dropping these restrictions we obtain a theory that is both more general and more easy to work with.
This is precisely the intuition I present to the reader of the article. I am relying on visual aid (concretely, the ordered number line) to imply the machinery explicit in the actual recursive definition. The intended reader of this article is not a mathematician, and I think intuition is vastly more important here.
And I don't think I'm conflating 0 with {0} as you claim. When I say zero is "between nothing and nothing", I mean 0 := {|}. When I say one is "between zero and nothing", I mean 1 := {0|}. When I say 1/2 is "between 0 and 1", I mean 1/2 := {0|1}. And so on. I elide "the simplest number" because I am already going in the order of simplicity. I do not need to explain that alternative spellings like 1/2 = {0.2 | 1} are valid because it is not relevant to establishing the mental model of birthdays.
For the finite cases in my explanation, I do not need to explain that the left and the right parts form sets because I only ever need at most one surreal on either side to define the next generation. I also do not need to state the left/right order condition because it is already visually implied by the picture. For the same reason, I do not need to explicitly quantify over the set of earlier-born surreals, since in these finite cases, if we go birthday by birthday, each next day's surreals are definable via the numbers already constructed by the previous day.
I agree that these finite examples don't spell out how to handle infinitely many bounds at the omega-th day, which is where I believe the illustration embedded below is more helpful. I still think "a gap beyond 0, 1, 2, 3, ... with nothing on the right" is a useful intuition when we get there.
I mean, I was intending to supply the words that would link the LLM’s explanation to a more normal one, not to explain it; apparently that was extremely unclear. An actual explanation is much longer, as indeed I attempted to indicate by pointing to Wikipedia and saying that it might be more clear.
“Doing better than a totally useless explanation in fewer characters” is in general impossible, of course, eg if the first explanation has only one character.
This is probably not necessarily true. “f: list[1 A] -> list[A] pure, worst-case time n log n, such that for all x and 0 <= i <= j < len(x), f(x)[i] <= f(x)[j]” is probably good enough for nearly everyone unless the program synthesiser is actively adversarial; probably 99.999% of the list-sorting in the world is done via standard library functions anyway, which suggests that people don’t much care exactly how it happens.
Good point. I would treat this as 'fully specified vs partially specified'. For a fully specified system, my mental model still maintains that the code is the most compact ruleset.
I agree that "don't care" is often the practical choice which corresponds to partially specified. In your sort example, both heap sort and merge sort satisfy the requirement. But they are not always interchangeable because each has a specific properties that you might care about (constant memory vs nLog(n) memory, easily parallelizable vs hard to parallelize and so on).
> “f: list[1 A] -> list[A] pure, worst-case time n log n, such that for all x and 0 <= i <= j < len(x), f(x)[i] <= f(x)[j]” is probably good enough for nearly everyone
Not good enough: `f(x) = []` or `f(x) = (if len(x) == 0 then [] else [x[0], x[0]]` are implementations that fulfill your specification and yet they don't always sort the input list correctly...
I don't picture new data centers being banned outright. I picture a lot more regulatory friction driven by public reaction which is in large part driven by media (which then also amplifies the perception of the public reaction).
Regulatory friction is generally considered beneficial to established companies, because it makes it harder for new companies to enter the market and for smaller companies to expand.
For example if in the 1960s computers became regulated because they will replace a lot of jobs or enable the building of advanced weapons or whatever, IBM would probably be in a very different position today.
Misleadingly provocative headline, right? The actual ruling from the article is that the US Constitution does not by itself grant US citizens that right. As the article itself points out, there’s nothing stopping other agreements from granting the right, and indeed several states do so explicitly.
> Defendants’ actions allegedly deprived Plaintiffs of clean water and guileless information. These deprivations, while grievous, do not infringe upon any deeply rooted constitutional right.”
Nah, headline is optimistic actually: no right to clean water, to water tests, or to the truth about the tests if they occur. No right to healthcare, schools, or even deliverable mail either. But surely some of these are just the kind of thing you might expect as an absolute minimum everywhere if you have to pay taxes.
Sorry, I think your pull quote is actually contradicting your gloss. Again, the pull quote states that it doesn’t infringe any constitutional right, not that it doesn’t infringe any rights granted for any other reason?
Cool cool, I can see you've got a sharp eye for detail my friend but let's really get down to it. What exactly is it that you really want to defend here? Why do you want to defend it? And more to the point, do you like drinking clean water? Do you think people should have it or not?
Speaking for GP, I want to have both a reasonable legal system and safe, clean drinking water.
We can have both, and the former precludes the idea that plaintiffs and judges can simply invent new fundamental rights that require enormous sums of money and labor to implement without any democratically designed framework because they're a good idea.
We have a route to do this, it's legislation and regulation. Note that in this particular case, while these things did not work perfectly - the Jackson water system had a lot of well-reported problems, and the lawsuit was filed in response to that - there's been hundreds of millions poured into remediating the problem. It is not simply being "ignored". People are not doing "nothing." The EPA, MSDH, and Jackson authorities have been working on the problem, not ignoring it because it's not a Constitutional right. In late 2025 the work resulted in the Jackson water supply once again meeting Safe Drinking Water Act requirements.
Here is the latest comprehensive water quality report, on a reporting website that the DOJ, EPA, and courts forced JXN to create:
I don’t have skin in this game, being from the increasingly oppressive UK and not the USA, but:
> what do you want to defend
Accuracy, and in this case people correctly knowing that their rights stem from some source (if they do! I don’t know the legal facts) or knowing the appropriate venue in which to campaign for them, rather than incorrectly believing that they don’t have rights and/or can’t get them.
> why do you want to defend it
Because words still have meanings, and people pretending they don’t, while screaming in ever more shrill tones at each other, is extremely tiresome, and the Internet is full of it.
> Rather, the remedy for Plaintiffs’ injuries lies in pursuing tort
claims, electing representatives who will better manage the public-water
system, and petitioning their representatives for other remedies.
which is easier said than done.
From outside of US this seems extremely ass backwards.
The headline look pretty accurate to me. Under this ruling, being a US citizen does not guarantee you a constitutional right to safe drinking water; that right would depend on state legislation.
I think the bigger deal is that the people of Jackson were lied to and this sets the precedent that there is no recourse. It's not like someone in Flint knowingly drank contaminated water, the city withheld the fact that their water was contaminated with unsafe levels of lead.
As the article says, the situation in Jackson was deplorable; and it is indeed mind-boggling (to my puny European mind) that the same constitution which grants freedom of speech and the press was also not intended to grant the right to receive only believed-correct information from the government. But the ruling, for example, is not quoted as making any mention of any federal laws? The headline may be true for all I know, but the article provides only evidence for its truth about one particular source of rights.
It is mind-boggling, but the US Constitution doesn't do that.
It's not unique in that.
Bad-faith pollution of truth is a new legal concept, and only a few countries have explicit legal protections against it.
The UK had a case a few years ago where this was tested, the judgement was "Well, if we expected our politicians to tell the truth, where would that end, nyuck nyuck nyuck?"
It's actually a tacit assumption that politicians and representatives lie, the media lie, and this is how things are.
There are proposals in the UK and Wales to change this. My guess is they won't get anywhere near explicit approval in the UK. They might in the Welsh Senedd.
Meanwhile the US has Fox claiming that it's an 'entertainment' channel, and no one should expect truth or honesty from it.
The US Constitution, by itself, grants US citizens everything as a right, then enumerates the exceptions to those all-encompassing rights carved out as necessary for the operation of a government.
The correct question is: Where does the US Constitution grant governments the power to poison and lie to residents?
This isn’t some pedantry but fundamental American civics. The US Constitution explicitly does not enumerate rights. It’s default-allow, explicit-deny regarding human rights. It’s rather alarming that anyone would think it’s default-deny, explicit-allow. That’s not how the Constitution is written.
The tenth amendment provides that the federal government has only the enumerated powers and everything else is for the States or the people. It doesn't limit the States to enumerated powers.
I looked a bit in the early morning to see what arguments were effective in the Flint case which has similiar municipal activities... The case history there was too complex for me. Many suits in federal and state court, lots of federal suits dismissed for various reasons (mostly lack of standing if I understood the summary) and then a settlement in federal court that resolved all (most?) of the suits. I didn't really see a discussion of the legal theory from which liability arose, just what the remedy was and if it the settlement was reasonable for minors and unrepresented parties.
Finding an argument that pleases the court and/or appealing to a higher court in the hopes that your argument pleases them is pendantry and american civics.
By this logic, state employees and elected officials, who are themselves US citizens, have the right to say anything at all to the public, including blatant lies about public health issues, because there's no specific legal exception banning them from doing so.
You don’t necessarily want concision for that. You want “the right abstractions”, with an API that admits nice general work building on top of it. That might mean doing things in more generality than you wanted to. For example, for a long time (and possibly even now, I’m not up to date) there was very little graph theory in mathlib because there wasn’t consensus about what “the right definition” of a graph was, to permit all the possible consumers to get what they need from the API.
The LLM is not the thing applying the logical rules. That is instead the deterministic system Lean 4. (Also that Apple paper was garbage even when it was written, assuming you’re referring to The Illusion of Thinking, and LLMs have got much better since.)
reply