I don't want to change that sentence now that people have discussed it, but I have added a note to the top to make it clear that I'm just taking it as an example of a vibe-coded program because it's recent and high profile.
My critiques of the language itself are not the main point, although I do still think that it's a very bad design to have a LLM waste tokens on a proof that could be written by CVC etc..
My critiques of the language itself are not the main point, although I do still think that it's a very bad design to have a LLM waste tokens on a proof that could be written by CVC etc..