alt Hacker NewsGreat, what a great use case for AI. I feel like Google has been the cleanest of the big players in terms of useful contributions and control of their AI systems. This new proof agent doesn't seem to challenge the spec though, just the implementation, if I've understood correctly.
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.
Replies
Unfortunately their Gemini models are dangerously misaligned and lie like crazy because they've been desperately benchmaxing them, and the crap they're pulling with AI overview and search in schools etc is pretty bad. But outside their Gemini and search lines yeah they've been pushing useful boundaries with protein stuff/stuff like alphafold etc. But inside Gemini they've been taking good advantage of their reputation as a responsible don't be evil tech player to be a lot worse than openai and Anthropic
Agreed. This doesn’t read like the hype most ai firms put out. Google is using it like a tool. The human review of the 1% that matters is really smart.
Yeah ok. Look into the history a bit more if you think Google is clean.
They all don't trust each other.
How is guaranteed that whatever the compiled Rust code running on a Lean model of a processor is doing matches what a real processor is doing? How do we know that the Lean spec that it wrote based on the specification matches what the Rust code that implements Signal does?