I've previously seen some ads for Claude on YouTube, mainly following the style of a programmer influencer talking about it. But I'm more of a technical audience.
Though, I happened to be watching the Superbowl, and Anthropic was all in taking pot shots at OpenAI's recent decision to start incorperating ads. Very much addressed towards a general audience. Here's one of them for example: https://youtu.be/FBSam25u8O4
Could it be since a lot of the data is trained on captions? At least if I'm remembering correctly, that's what they use to create the association between what's seen and what's said.
I've heard this can be a bit of a pain in practice, is that true? I can imagine it could slow me down to construct a proof of an invariant every time I call a function (if I understand correctly).
I haven't worked significantly with lean but I'm toying with my own dependently typed language. generally you only have to construct a proof once, much like a type or function, and then you reuse it. Also, depending on the language there are rewriting semantics ("elaboration") that let you do mathematical transformations to make two statements equivalent and then reuse the standardized proof.
I feel like that's a rather bad-faith take, so if you're going to make that kind of accusation you better back it up. People can legitimately believe that AI is not going to be the end of the world, and also not be privileged. And people can be privileged, and also be right. Not everything can be reduced down into a couple of labels, and how those labels "always" interact.
Wasn't that the point of mentioning Jevon's Paradox though? Like they said in the essay, these things are quite elastic. There's always more demand for software then what can be met, so bringing down the cost of software will dramatically increase the demand for it. (Now, if you don't think there's a ton of demand for custom software, try going to any small business and ask them about how they do bookkeeping. You'll learn quite quickly that custom software would run much better than sticky notes and excel, but they can't afford a full time software developer as a small business. There's literally hundreds of thousands of places like this.)
Regardless of whether this means AGI has been achieved or not, I think this is really exciting since we could theoretically have agents look through papers and work on finding simpler solutions. The complexity of math is dizzying, so I think anything that can be done to simplify it would be amazing (I think of this essay[1]), especially if it frees up mathematicians' time to focus even more on the state of the art.
Maybe the best thing to say is we can only really forecast about 3 months out accurately, and the rest is wild speculation :)
History has a way of being surprisingly boring, so personally I'm not betting on the world order being transformed in five years, but I also have to take my own advice and take things a day at a time.
I will say one thing Claude does is it doesn't run a command until you approve it, and you can choose between a one-time approval and always allowing a command's pattern. I usually approve the simple commands like `zig build test`, since I'm not particularly worried about the test harness. I believe it also scopes file reading by default to the current directory.
reply