Hacker News new | ask | show | jobs
by saithound 119 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.

1 comments

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.