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
1d 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
1d 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
1d 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
2d 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
2d 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
2d ago
I didn't think you were the kind of guy who takes tech demos seriously.
sarker
competency crisis actor
2d 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
2d 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
3d 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
3d 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
3d 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
3d 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
4d 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
5d ago
LLMs are excellent for recommending textbooks or other study material.
sarker
competency crisis actor
5d 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
5d 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.
sarker
competency crisis actor
7d ago
Is a train derailment really a "weird" thing? It's a rare event, but they do happen.
sarker
competency crisis actor
7d ago
You'd think they'd charge more so they can launder money faster.
sarker
competency crisis actor
11d ago
Sure, but you don't need a great man to see or execute the path to success. Seldon did not foresee Hardin and Hardin's untimely demise would not have mattered.
sarker
competency crisis actor
11d ago
The whole conceit of the "seldon crises" is that there's only one way out of them. Do you need a great man for that?
"No! Hari Seldon said in the Time Vault, that at each crisis our freedom of action would become circumscribed to the point where only one course of action was possible."
"So as to keep us on the straight and narrow?"
"So as to keep us from deviating, yes. But, conversely, as long as more than one course of action is possible, the crisis has not been reached. We must let things drift so long as we possibly can, and by space, that's what I intend doing."
sarker
competency crisis actor
11d ago
The practice of mathematics involves writing proofs in a heavily intuitive manner, and their verification in turn involves people who have been socialised to share the same intuitions
I'm struggling to understand what you mean. At this point we have systems for automatic verification of formal proofs. In what sense are those systems socialized to share the same intuitions?
sarker
competency crisis actor
11d ago
The idea is that if the labs were to coordinate a pause in frontier AI development, this would be a "conspiracy in restraint of trade" and therefore illegal.
We don't have to speculate.
We request that the U.S. government support an international effort to develop the technical and governance tools needed to deliberately pace the frontier of automated AI development.”
To a first approximation, if the government tells you not to do something, it isn't a crime to not do it. The coordination for a pause has always and everywhere been at the level of international governmental treaty.
Please don't @ me about how this will never happen; that isn't the point, the point is that the proposal isn't a gentleman's agreement between competitors.
And how big is "star" as far as stars go?
More options
Context Copy link