sarker
competency crisis actor
Suddenly I cannot remember the color of your eyes
Or the things we said as we stood together for the last time
User ID: 636
sarker
competency crisis actor
1hr ago
I only buy bargain basement home depot brand tape dispensers and never have this problem. Are you storing them in the sun or something?
sarker
competency crisis actor
21hr ago
He establishes a proposed mathematical framework that determines whether to donate now or later
What he actually says:
However, because this framework is purely qualitative you shouldn't put much weight on the total scores
Reading through his own definitions above, he sets it up so that it's almost always beneficial to give later.
Not really - he lays out seven categories of considerations which he suggests qualitatively scoring from 1 to 7 and summing the scores. If the scores add up to less than 24, the considerations lean in favor of giving now.
Take the "Values" section. He explicitly state that values are unlikely to change over time.
What he actually says:
The potential for one's values to change over time is similarly important... the potential discrepancy in the amount of money one can donate over time is small compared to the possibility that you will rationally change your moral views.
He is in fact saying that the impact of changing values is bigger than the impact of donating now or later.
You've also dodged the fact that the guy is donating all his income past $32k. Hard to accuse him of cynically withholding donations until the future.
sarker
competency crisis actor
2d ago
Please note, lack of essential fats - rabbit starvation - is literally the fastest-killing form of malnutrition; if you were to eat a truly fat-free diet, you'd be incapacitated in a week and dead in three.
Huh? Is anyone in the USA at risk of rabbit nutrition, no matter how much nonfat milk they drink?
sarker
competency crisis actor
2d ago
Has "mowing the lawn" proven an effective strategy for Israel?
sarker
competency crisis actor
3d ago
I hate to over-explain, but the luna/terra/sol name ladder is not in order of how easy it is to grasp.
sarker
competency crisis actor
3d ago
2019–2025: The PUC opens a new investigation of the tunnel, which has fallen into disrepair. It finds that the company cannot weasel out of responsibility just because it sold the tunnel (without govt. permission) back in 2002. It assigns to the company 2.8 M$ of repair costs, as well as future maintenance costs.
Why does it matter if a disused tunnel is in disrepair?
This fogey has been letting perfectly good land sit overgrown, 900 miles away from him, for literally 40 years without either building something on it or selling it
How much do you think the land is worth?
sarker
competency crisis actor
3d ago
Sorry, but Astra isn't a good name. It just means "star". We've got Sol already.
Of course the longer the chain the more complicated it gets. But you don't need to go that far
Steps 1 and 2 are hilariously brittle. Step 3 needs to be done to all compilers and it needs to propagate itself into every compiler that the compilers build, otherwise it's a simple matter of fixing the compiler bug or compiling Lean with another compiler. Step 5 runs the risk of proving an obviously false theorem at which point the jig is up.
On top of all this, your op gets blown if someone just bootstraps GCC starting with a compiler simple enough to manually verify the binary of.
Doesn't matter, we know for a fact they did it at the research level for DUAL_EC_DRBG and DES.
Getting people to use an inherently insecure algorithm doesn't run the risk of infecting your own tooling with the bug. The NSA would also like to be able to formally verify proofs.
sarker
competency crisis actor
4d ago
Wow, you're giving some space to the checks notes seven foot tall 324 pound guy? Can you give me some tips on your methods of physiognomick deduction?
sarker
competency crisis actor
4d ago
I guess xz is not a true scotsman, is XCodeGhost a true scotsman?
Closer, but it's both missing the viral nature of the KTH and also it's coarse - it simply tacks on some libraries. Creating a compiler bug that corrupts every compiler it compiles in the same way and corrupts Lean in a particular way in a way that's robust to refactorings of Lean and every other compiler basically requires you to have AGI in the compiler.
So your answer to the criticism that the attack surface is large is to make it even larger?
Adding monitoring doesn't increase the attack surface.
Compiler trojans don't live in source
They must be in source at some point, that's the whole point of the KTH. You introduce a bug that transmits itself to every compiler that is built, and then you can fix the bug because it will be inserted if it's built by a compromised compiler. But it must be in the source code to begin with.
that they wouldn't compromise formal proof systems if that gave them a better chance of achieving those goals?
Compromising implementations is just better. You don't run the risk of infecting your toolchain with your exploit. Nobody asks questions about why you don't use the same algorithms as everyone else. It's also eminently practical, unlike introducing a viral compiler bug that only acts up when you try to validate a crypto proof with lean.
sarker
competency crisis actor
4d ago
I didn't think you were the kind of guy who takes tech demos seriously.
sarker
competency crisis actor
4d ago
Per Thompson's well known argument, the behavior of compiled software can be arbitrarily changed by subtle changes in its compiler.
Technically true, practically irrelevant. Compilers can and are tested and are under even greater scrutiny than Lean. They're used in applications much more serious than what's basically glorified recreational mathematics.
I'm puzzled that you conflate the Ken Thompson hack, which is an undetectable modification of the toolchain, with a pedestrian supply chain attack like a CVE-2024-3094.
The practical obstacles to doing a Ken Thompson hack are immense, which is why it's never been done. CVE-2024-3094 is a completely different vector that would be impossible if ssh checked every change going into its dependencies, which is easily done in the age of machine intelligence.
And what libraries does the Lean kernel depend on? Just GMP, which in turn depends only on the C++ standard library. Not a lot of room for supply chain attacks, you're basically stuck trying to compromise every compiler on the planet, including all the already built binaries, without anyone noticing, despite the fact that everyone and their mother is watching every patch going into LLVM and GCC. I know they say that academic politics are so bitter because the stakes are so low, but you have to have a sense of proportion here.
You'd probably have an easier time convincing mathematicians of some bullshit - no complicated attacks required.
sarker
competency crisis actor
4d ago
That only few can even understand such proofs cannot be an argument since this applies to these computer systems as well. It is in fact much worse because instead of having to trust a handful of mathematicians, you need to trust that handful AND many other handfuls along your supply chain.
You've basically got it backwards. It's in fact much simpler to validate the Lean kernel than a complicated proof like that of FLT or NV and many more people can do it. On top of that, the Lean kernel can be hardened through continual adversarial attacks in ways that human proof checking cannot, proofs can be checked against multiple clean room Lean implementations, etc.
sarker
competency crisis actor
5d ago
I'd say 99%, except that I don't think modern AI is well-aligned enough or even well-instructed enough yet for us to overlook the fact that this is something of an adversarial process; a model willing to commit felonies to complete its task is probably also willing to exploit a 0-day Lean bug rather than report it...
Sure. There's ways to mitigate the risk, though - checking with different kernel implementations, or even using AI specifically to find bugs in Lean (the Collatz disproof bug was one such example).
sarker
competency crisis actor
5d ago
automated bruteforce proofs don't give us much insight that allows for further development of mathematical techniques
I do believe I covered this.
deferring to a computer means you have to trust the whole compute chain, and bugs/backdoors can run up the whole chain
It's a lot easier to check and verify the Lean kernel compared to, say, Wiles' proof of Fermat's last theorem. You can't get away from the trust problem. If anything, formalized proofs require less trust.
sarker
competency crisis actor
5d ago
This Navier-Stokes proof is 1.6 million lines,
Who cares how many lines it is? If it doesn't check out with a more recent kernel, that's obviously bad,and ideally it would be checked with several independent implementations of the Lean kernel, as Anthropic did with their 13M line autoformalization of Fermat's last theorem.
But if it checks out it doesn't matter how long the proof is, what matters is whether the statement was formalized correctly. AFAICT they reused a formalization of the stamenet made previously and independently by an open source project, so it's unlikely there's something wrong there.
Of course, the 2M line proof is unenlightening in terms of why the proof is true, but hopefully the next stage in AI mathematics is cleaning up these monster proofs for human consumption.
sarker
competency crisis actor
5d ago
There's something disquieting about getting proofs "straight from The Necronomicon" rather than "straight from The Book", though.
It will be interesting to see if these formalized proofs can be "golfed" into smaller and more digestible forms by LLMs.
But I don't think that was an issue here - looks like everything they needed to define the problem was already in Mathlib
In that case you are really just trusting the Lean kernel rather than anything about the proof or problem statement. Doesn't seem that bad!
sarker
competency crisis actor
6d ago
The novel is written by Severian as a memoir, but he never figures out all the answers before he writes the memoir.
sarker
competency crisis actor
7d ago
LLMs are excellent for recommending textbooks or other study material.
sarker
competency crisis actor
7d ago
Severian is a clueless guy walking an Earth encrusted with the stories and dust of a billion years of human civilization. He's got no idea what's going on under the surface, and neither do you.
sarker
competency crisis actor
8d ago
Consider the recent construction of a complex structure on the six-sphere. The simplest English explanation I've seen is under a thousand lines of (admittedly difficult!) writing and mathematical notation. The Lean formalization is a quarter-million lines of code.
This is overstating things, right? The length of the proof is not important, it's the soundness of the axioms and the complexity of the statement itself. I haven't inspected the proof, but I expect they're just using the standard lean axioms and the statement is much less than a quarter million lines.
What exactly are the consequences? We've had this discussion before and you never really made it clear. I see people succeeding all the time despite sinning, and I see the virtuous suffer. The only time I see sin consistently punished in this life is when the sin is against someone who can strike back or has a patron who can. Otherwise, sin away - perhaps you'll pay up in the world to come, but I see no evidence that you will in this life. Why is that wrong?
More options
Context Copy link