This is the first time I've seen a complaint about giving permission to an app to install another app. The SmartTubeNext issue was due to the developer's keys being stolen. If you want to keep an app signed with stolen keys, you can disable Play Protect. If Play Protect uninstalled apps that Google disliked instead of apps with known vulnerabilities, people would mass disable Play Protect, which would defeat its purpose.
Even the meta version is picky about where it goes. The whole declaration has to fit inside the first 1024 bytes. Easy to break with a giant comment at the top.
Maybe I'm misunderstanding something about how all this works, but can we have any confidence that 13 million lines of AI-generated Lean code are... correct?
How have we not merely substituted one verification problem for another?
Not always, there can be bugs in lean. Recently some guy with claimed to disprove Collatz conjecture, only to turn out that there was a bug in lean. I actually have no idea, how anyone can be sure this 13 M lines is meaningful
Lean is adversarial in a way. Lean is better thought of as a constraint language with a verifier that checks if the constraints are respected, than a programming language.
Your job or the LLM's job is to write code that Lean is satisfied with, creating the link between what you're trying to prove, and mathematical axioms.
If you write a bad proof, the Lean constraint checker will tell you, unless there are bugs in Lean itself, or you defined the goal constraint incorrectly.
The discussion of "FLIP (First, Last, Invert, Play)" would be improved by mentioning the View Transitions API, which is basically there to automate this technique.
We are fortunate that this individual's stylistic perspective is out there adding spice and variety to the world. I think, however, that most of us would be ill-advised to emulate it.
Orwell's maxim, "never use a long word when a short one will do", is something the best writers have always freely ignored. But it's a reliable guardrail for the writer of merely average skill, steering them toward something passable rather than vomit-inducing.
The map tile backend is in the middle of a multi year effort to migrate from the Flippity Service to the Floopity Service. The FlippityFlooper was believed to have finished the necessary format conversions for all map tiles in the US and Canada but 5% of the data sources were missed due to a bug that was discovered after the creator of FlippityFlooper had been promoted and changed teams, so those Floopity tiles are filled in from an older source. A junior engineer vibe-coded a stopgap fallback called FloopityFlipper that redirects to legacy Flippity Service when Floopity staleness is detected, but that redirect broke three months later due to a change in an injected dependency's experiment configuration. A bug was auto-filed and marked P2 by an overworked product manager who slightly misunderstood the scope, but the FloopityFlipper engineer will probably have a look once they are back from paternity leave.
I made all of that up but it's more plausible than conspiracy theories.
reply