The fact that the description is AI slop doesn't inspire confidence in the results.

Slop Verbiage, Straight To Your HN Feed

browningstreet a day ago | parent | prev | next [-]

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 14 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 8 hours ago \| parent [-]
		> What a time to be alive. That's way more infuriating than hackneyed AI copy.

▲

joe_the_user a day ago | parent | prev [-]

Yes, "This milestone begins with the Stacks Project itself". Could half AI slop effects be mitigated by a prompt "Don't mix or mangle metaphors here"? A milestone is a step in a process, not the entire process.

Once this kind of sloppy effort to sound impressive was just "over writing" but its now a strong tell for AI.

▲

falcor84 a day ago | parent [-]

Why is that a mixed metaphor? I'm very used to large initiatives/programs with several large milestones, each involving multiple projects. I don't see any issue with it.

	▲	joe_the_user a day ago \| parent [-]
		The milestone they are reaching is the formalization of The Stacks Project. It began whenever they started prompting an AI to do that or started preplanning. The metaphor of milestone is a goal reached within a larger process. I think that, yeah many people will not find a problem instances of this sort of (mis imo) usage but AIs to create a sequence of these things and that tends to create a tone to AI writing that many people can feel even if they can't point to particular problem usage.