danabramov

If I leave Astra overnight, I'll wake up with three new different projects, each of them 20% done and having nothing to do with my original goal.

Re: "rich", I've essentially spent $400 on this (in subsidized subscriptions), plus my free time being a mindless drone. Given that you assume my role is automatable, it sounds like this is relatively accessible to anyone with $400 (as long as AI companies continue subsidizing the frontier models). I don't think I've had some kind of an unfair advantage beyond that. If anything, a proper mathematician would probably be able to derive the result much faster with the same tools.

I don't know how the broad availability of these tools (to mathematicians and non-mathematicians alike) will change the field, what is considered prestigious, what work gets funding, how it affects the pipeline, etc. You seem to be implying that even testing the limits of these tools, or at least publishing the results obtained with them, is unethical in itself, even though it is broadly accessible now. I can understand this point of view.

I am not saying that my work constitutes a mathematical contribution on its own. Not any more than stumbling upon an anonymous manuscript with the solution would constitute a mathematical contribution. I do, however, think that it can lead to a mathematical contribution if any mathematicians consider it worthwhile to do something with it. Whether or not they consider it worthwhile is not up to me.

It might be possible to plainly continue-shot it with more powerful models in the future. I agree that whatever I did is probably automatable.

The alien in the analogy is the corpus of knowledge that’s newly reachable via LLMs.

Would you, in this situation, be mad at the aliens? Would you say the aliens have "extracted value"? This is kind of how I see this project.

I do that too when working on software. Here, I did a little bit of that, but it is much harder when I have almost no domain knowledge (aside from understanding the statement of the conjecture), since at each point the LLM might trick me anyway, and it would probably take me a year to understand the concepts enough to tell when what it's saying doesn't make sense.

>Even just keeping the Lean more up to date would have likely saved tokens

That's the conclusion I came to by the final week! But don't underestimate how much Lean needed to be written in the first place to even "catch up" with the reference papers. I had no option to keep it up to date when I started.

Yes, I was not doing any mathematical work in curating the output, but the article makes it quite clear that pivots and constraints the LLM would not impose on itself were critical to actually making progress.

Also:

>He doesn’t even know any mathematics and has never cared to learn

While I don't know enough mathematics to work on this problem, claiming something like this is preposterous. As I link in the first paragraph of the article, I've been learning mathematics on my own by going through Terence Tao's Analysis book and solving exercises. I'm familiar with the concepts of mathematical definitions, proofs, etc. I've gotten about halfway through the book solving them on paper before abandoning it (and later got through the first few chapters in Lean, also solving every exercise — by hand, mind you). Sure, this doesn't make me a mathematician, but I'm closer to a dropout first-year student than to someone who has "never cared to learn".