zaxioms

9 ms·

1.
by zaxioms 7mo ago
If you wanted to implement this in real life, who plays the role of Alice?
2.
by zaxioms 8mo ago
> Blake embodies the “bits to atoms” shift underway in America. Before founding Boom, he was designing internet coupons for Groupon. What is this? I can't find easily the meaning of "bits to atoms." Is this meaning that US
3.
by zaxioms 10mo ago
Ok I guess I could have told you that. What I really meant is that in the future where LLMs are doing new math (which I'm skeptical of, but I digress) I would not trust any of it unless it was formally verified.
4.
by zaxioms 10mo ago
It's cool, but I genuinely cannot fathom why they are targeting natural language proofs instead of a proof assistant.
5.
by zaxioms 11mo ago
Does anyone have a similar article with more detail? I don't quite want to read the datasheet of your favorite microprocessor, but I would like a decent amount more detail than what's provided. Especially before UEFI/BIOS.
6.
by zaxioms 1y ago
Rice's theorem is about decidability, not difficulty. But you are right that assuming P != NP there is no algorithm for efficient SAT (and other constraint) solving.
7.
by zaxioms 1y ago
I'm surprised to hear this. Modern SAT solvers can easily handle many problems with hundreds of thousands of variables and clauses. Of course, there are adversarial problems where CDCL solvers fail, but I would be fascinated if you can
8.
by zaxioms 1y ago
I'm fascinated that Epic Games are the authors. Does anyone know what their motivation for this research would be?