Comment by saithound
2 days ago
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!
Should have used ultrathink. I'm disappointed this is not called deep thought.