I wonder how this agent is different than a classic coding agent, in the end it seems to work the same way, iterating over a codebase while writing Lean or Rocq code and running it.
I would be extremely impressed by a robot that swam the Atlantic or climbed Everest, as would almost any human alive. If you have a robot that can do one of those things, you should absolutely do it as a publicity stunt.
This is yet another example of OpenAI getting distracted by shiny things while the rest of the ecosystem focuses on solving real world problem scenarios with market potential.
That shiny thing persuaded me, a grizzled veteran inclined to doubt every latest fad almost on principle, that AI is already much more powerful than I thought was possible. This is the second time I've experienced such a shift, the first being when I watched an AI spit out a complete working program in response to a paragraph of text just a few short months ago.
Or you can use verus instead which does automatic mapping from the rust code to the proof where possible.
Compared to the other LLMs I've used, it seems to have system instructions that are far more adversarial to the user.
Aggressively staggeringly high rates of straight up making shit up and covering up the lies. Gemini 3.5 flash was comical because it would delusionally scream nonsense like "we're go-go ready!!! :tada:" while the code didn't compile (I swear the only reason people thought that was a good model was because they didn't use it) and their models just got better at making tool calls without fixing it's tendency to cheat.
Gemini models are not looking all that good here: https://maxxbench.unlap.ai/
They got a lot of shit for it at the argon launch and you'll notice the carbon release blog has a lot of detail on how they focused on misalignme t and fabrication rates: https://blog.google/innovation-and-ai/models-and-research/ge...
So Google themselves is not behaving like they think people are making stuff up about their models behavior.
Google itself is also just behaving in such a sleazy way. "Carbon is the best model ever but also you can't use it yet." Watch them release it now that fable is out and nobody cares anymore so nobody checks to see how much they benchmaxed lol. They're clearly under some sort of internal pressure to pretend they're at the frontier and that's bleeding through I to the frenetic pace of model releases they've had in the past couple months through Argon and Carbon. Bleeding through in the sense of the models also only really care about benchmarks and good news cycles. Again they did claim they tried to solve a lot of this for carbon but they didn't let people use the model and once you have a base model that cheats benchmarks you have to wonder if it actually lies less or just gets caught less, but hopefully they got things back on track?
Fucking called it: https://blog.google/innovation-and-ai/models-and-research/ge...
They've been releasing their models 2 weeks after the first announcement. I doubt Google is timing their GA against Anthropic unless they had knowledge of when exactly Anthropic was releasing theirs.
Also, I've been using Carbon vs Opus 5.5 and Carbon is a great model. Haven't seen any hallucinations. Argon was well known to be a worst programming model than Opus via benchmarks, so you and influencers broadcasting a well kept secret.
They all don't trust each other.