What if you asked your favorite AI agent to produce mathematics at the level of Vladimir Voevodsky, Fields Medal-winning, foundation-shaking work but directed toward something the legendary Nikolaj Bjørner (co-creator of Z3) could actually use?

Well, you'd get this embarrassing mess, apparently.

That’s because they didn’t add “and don’t make mistakes!”.

And yes, the exclamation mark matters!