Smaug123

7 ms·

1.
by Smaug123 6d ago
The question pertinent to your decision is "do I want to see more of this on Hacker News, or less?".
2.
by Smaug123 7d ago
Would it? Don’t they all desperately want more compute, and not the banning of new data centres?
3.
by Smaug123 10d ago
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
4.
by Smaug123 11d ago
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 rece
5.
by Smaug123 11d ago
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?
6.
by Smaug123 11d ago
Does it? I think that conclusion requires observing additionally that all federal law also fails to grant a right to safe drinking water, doesn’t it?
7.
by Smaug123 11d ago
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 gra
8.
by Smaug123 11d ago
It’s an aggregated list, not a list of formalisations in Lean - the checkbox is “things formalised in any prover”.
9.
by Smaug123 11d ago
Because you wrote: > what are exactly rules, which could be separate topic of research, this detail is skipped I am now confident you’re a troll, though, so I am going to bow out.
10.
by Smaug123 11d ago
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 countere
11.
by Smaug123 12d ago
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 t
12.
by Smaug123 12d ago
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
13.
by Smaug123 12d ago
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!
14.
by Smaug123 12d ago
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,
15.
by Smaug123 12d ago
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 the
16.
by Smaug123 12d ago
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
17.
by Smaug123 12d ago
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, slig
18.
by Smaug123 12d ago
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 L
19.
by Smaug123 13d ago
I claim that the percentages add up to more than 100% because the first described case overlaps with the second.
20.
by Smaug123 15d ago
It doesn't necessarily change the output distribution; it depends exactly how it's implemented, and Anthropic haven't told us that. Google's original SynthID paper describes how you can do this. Toy proof-of-concept: Ant
21.
by Smaug123 15d ago
G-Research | https://www.gresearch.com | London UK, on-site | Full-time G-Research is a leading quant finance company. Big compute farm, interesting problems. My team is hiring senior engineers to work on our (actually world cla
22.
by Smaug123 19d ago
You didn't name the object when you said "let this thing be X"; you actually had already identified that "thing", and that process of identification was the process of naming it. You then defined some syntax (&quo
23.
by Smaug123 19d ago
> no one has found one More than that: there is no way to build one (assuming the word "build" means some concrete construction), because it's consistent with ZF that the reals admit no well-ordering. Indeed, you can use f
24.
by Smaug123 20d ago
I’m afraid human red-teamers against supposedly highly secure targets, with lots of protocols in highly policed settings, do frequently manage this kind of social engineering. There’s loads of stories of pentesting military establishments,
25.
by Smaug123 20d ago
They didn’t intend to give it Internet access. Artifactory is a caching proxy which can be scoped to specific package ecosystems, not a general Internet gateway (unless configured that way).
26.
by Smaug123 21d ago
Because we should not settle for building a world in which every interaction must be assumed adversarial! Obviously risk reduction processes are good because they reduce risk, but we should not accept building entities which are actively tr
27.
by Smaug123 21d ago
For reference, this is Yudkowsky's "Law of Earlier Failure", which he has most charitably stated as: > Compared to the interesting part of the problem where it's fun to imagine yourself failing, you usually fail befor
28.
by Smaug123 21d ago
In my understanding, "e/acc" usually means "full speed ahead, humans aren't the optimal species anyway" for whatever bizarre definition of "optimal" they use, so my model predicts that they would wel
29.
by Smaug123 21d ago
This is not a very actionable reply to "well, what will you do when it's crossed?" - how on earth am I supposed to unplug AWS Bedrock and Colossus and OpenAI's own servers?
30.
by Smaug123 21d ago
In fairness, while the swarm could easily have notified the humans, it's not necessarily obvious that an individual could have done easily (though perhaps one could!). The channel to the Internet was tightly bandwidth-limited, for

More ›