Remix.run Logo
▲ browningstreet a day ago

Axiom raises $264M, publishes this massive lean proof built with AI, and you're moaning about some AI language in their description. AI is in their domain name. What are you doing?

▲breezybottom a day ago | parent | next [-]

With that much money you'd think they could hire someone who took a writing class.

▲joe_the_user a day ago | parent | prev [-]

Using AI isn't an excuse to use it badly. I mean, it's the constant excuse but shouldn't be.

▲nh23423fefe a day ago | parent [-]

what's bad about it? formless assertion has no content

▲joe_the_user a day ago | parent [-]

I mentioned one AIism here: https://news.ycombinator.com/item?id=50383112

And here's another example of mangled word use: "creating a sweeping dictionary between algebra and geometry that allowed mathematicians to do geometry over arbitrary rings, with arithmetic and infinitesimal data built in from the start."

What does "sweeping dictionary" mean?! And I don't think "creating ... across" is the right to way to construct indirect objects. In old writing day I think it would be called an "awkward construction" but I everyone's very used to such awkward constructions AI tells.

Consider they/it could have said "creating a link between algebra and geometry that allowed mathematicians to do geometry over arbitrary rings, with arithmetic and infinitesimal data built in from the start. ", in fact that's the language I'm used to.

It's shame because twisting metaphors in an ad-hoc way can be a nice thing but LLMs do this constantly and badly and mother looks at the (simulated) kids and says "this is why we can't have nice things".

Edit: I can't help myself "...In a tightly interconnected dependency graph of definitions and theorems..."

Sure, connected and interconnected mean nearly the same thing. But graphs in mathematics are spoken of as connected, not interconnected. Again, subtle usage but bad subtle usage adds up, damn it.

▲twoodfin 13 hours ago | parent | next [-]

“… built in from the start” is also hackneyed, and doesn’t fit the dictionary metaphor.

▲a57721 a day ago | parent | prev [-]

> sweeping dictionary between algebra and geometry that allowed mathematicians to do geometry over arbitrary rings, with arithmetic and infinitesimal data built in from the start.

That made me laugh, I wasn't expecting grothendieckian geometry to be described in LLM speak. What a time to be alive.

▲browningstreet 7 hours ago | parent [-]

> What a time to be alive.

That's way more infuriating than hackneyed AI copy.