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.)
Fortunately FLT is an extremely simple statement. Much easier to satisfy yourself that its statement is what you wanted to say than it would be for most statements of interest!
Claude’s formalisation, being in Lean, is based on the calculus of inductive constructions, not ZFC. In Lean 3, per Carneiro, any theorem of Lean 3’s theory can be proved in ZFC plus some finite number of inaccessible cardinals (and, IIRC, vice versa). The precise strength of Lean 4 is not quite clear yet, I think (I guess this is partly what Lean4Lean is hoping to address).
It simply does have functions. According to ZFC, a function is a set whose members are pairs, such that no two different pairs have the same first element.
I mean this quite seriously: have you considered reading any first course in set theory?
As I have said a few times now, you should read any first course in set theory. I’m quoting my third-year notes from Cambridge there, but essentially every intro to set theory will say the same. (I’m sure someone will find a single counterexample that does it somehow differently.)
Eh? Any first course in set theory will present ZFC as a one-sorted theory with ten axioms (/schemas) in first order logic (inheriting an equality symbol, forall, implies etc) with one binary predicate (namely set membership), or will present a theory that is equiconsistent with a usual ZFC presentation. Honestly I’m not sure how you simultaneously claim to be a PhD in formalisation and also not be aware of the existence of Isabelle/ZF, for example.
I referred to specific definition in wikipedia.
Your "first course notes" are irrelevant here, they can't be reviewed, they not proofread and unlikely can be considered as any reasonable quality if we are talking about real formalization of math.
It is possible, although the post notes that the proof was also verified by the Comparator, which means any exploited bug has to also be present in that checker. Which is not unheard of, but is much less likely than merely an exploit in Lean 4.
The comparator was only used to verify that the final statement indeed is a valid formalization of Fermat's Last Theorem, not that the proof leading up to it is correct.
I think this isn’t true? Comparator verifies proofs; it’s not clear to me what it even means to mechanically verify a statement to be valid. The statement is manifestly valid anyway - it’s hard to find much simpler statements of maths, slightly odd facts of mathlib’s natural arithmetic like the saturating behaviour of natural subtraction notwithstanding.
reply