How refreshing to read the thoughts of a human in a blog post instead of the garbage that LLMs produce. As the writer says about some of their proofs, the problem is not one of style or em-dashes, but something deeper about the writing that comes out of LLMs:

The problem is it doesn’t make any goddamned sense.

I'd probably insert a 'sometimes' in there, because many times in small doses it does make sense, it's only when you ask for long form writing/work that it becomes apparent there is no coordinating intelligence there.

Interesting just how much of this advice applies to programming as well as to maths:

--

Skills, agent.md and harnesses are probably a dead-end that will die off as the tools become more capable.

LLMs are not good at reducing complexity, however they're very good at adding it, and sometimes it is just unnecessary and he can find ways to cut it by interrogating the LLM.

Some people are responding to the new reality by gleefully using AI to generate lots of semi-OK-ish papers and puking them up on arXiv [this is like people producing mediocre one-shot clones of software].

On the other hand—with creative writing, my advice is not to use AI to write, at all. Ask questions if you want, but write every damned word yourself.

--

Definitely worth a read for the programmers here too.

"If you just waited a year, would some other AI produce that same proof independently?"

I had a conversation about this very problem last November, with a visiting mathematician. It's essentially signaling a deflationary spiral in intellectual work: why bother doing the work now, when it will take half as much effort a year from now?

This is perhaps always a possible stance, but it's exacerbated when some proportion of your own agency is handed over to, well, agents.

>But maybe that’s still just making the proof easier for humans to understand? No! For one, this usually makes the proof shorter, and sometimes dramatically shorter.

Hmm, so is the way to train this to take all the long complicated proofs it generates in Lean and then use autoresearch to minimize the length of the proof?

My priors have been so thoroughly updated by all the recent progress in AI that it really seems like there isn't anything that fundamentally cannot be learnt. So, is this how we train this kind of taste?

I'm not a mathematician, nor an AI engineer/researcher. Just watching from the sidelines and spitballing ideas.

What a time to be alive?

this is a great and wonderful contribution. best thing i have read on this.

related

Lex Fridman recent podcast on the AI crisis in math, https://youtu.be/ZAzWPE9CItg

Point 19, right in the feels :(

The overselling of AI abilities is doing such a disservice to society right now. These companies don’t want to acknowledge how much human collaboration is going into their AI’s achievements because it undermines their value proposition, but I imagine there’s still quite a fair amount going into it and that’s one reason why OpenAI still won’t provide session traces of their models solving open math problems. If they were more transparent about it I think we’d see that human guidance, vision, judgement, taste, and other traits are still highly valuable and complimentary to AI abilities. It should also be a huge red flag how little of any of this output has been formally verified by third parties. I do think AI will eventually do all the things people believe it’s already doing, but I suspect there’s a fair amount of mechanical turking going on behind the scenes as you’d expect any company trying to raise a trillion dollar public offering might do.

This is very similar to how I feel programming.

What's a Kofuni expansion?

These mournings of programmers and now mathemathicians will as time goes on likely continue to become a part of other fields workers routines as well.

I wonder how we as a society will react to this, this crisis of meaning. Not to get into existential crisis if that is to happen as well, which of course is a whole other issue.

I assume we will all start to look for social ways of mourning with colleagues.

It’s funny how disconnected we all are from each other. This is exactly how LLMs felt a year or so to many programmers.

Useless toys, sometimes useful toys, ok good toys, ok.. we might have to look at this more carefully, oh god.

This loop however is quite tiring to watch happen over and over again. Is there really nothing we can do but just watch from the sidelines and watch our fellow men engage in their particular grief and copium filled mourning cycle?

> I think the biggest reason I’m not more productive is: What’s the point? In the past, if you came up with an elegant proof, you’d tell yourself, "I made a thing! Other people will read and use my thing! I am advancing human progress."

This is so relatable.

I've always been very self-motivated and keen to dig deep into things and create difficult stuff, but these days I just see no point learning or doing anything...

Everything that used to give my life colour seems completely pointless now...

Learning new algorithms, creating open source projects, writing music, writing about tech, etc.

I know people say that it's great and now we all get to spend more time going for walks and watching TV, but it all feel kinda empty honestly. My fun was always doing difficult stuff and feeling that joy of working it out or giving the world something cool. But now, for the first time, I feel I have nothing to offer anyone.

About two years ago, I was at a coffee shop and two maths students were trying to understand a concept in the book. I suggested they might ask a language model to help them understand it. They scoffed at me, called a stochastic parrot, and said they can't do math at all.

I responded with, "Well, you don't even need it to do math. It can explain the concept." They scoffed again. "Those things are useless toys"