alt Hacker News> The content in Mathlib still falls very much short of being enough for formalizing much of the actual research being done in mathematics, but people are now autoformalizing non-trivial extensions on top of that,
Formalising non-trivial extensions on top of the standard library is not hard. I could bash out an average textbook formalisation at about half reading speed. The hard part is making something elegant and general, which: and that's something that LLMs don't seem able to do.¹ (If you're lucky, the textbook you're working from has already distilled the best abstractions, and there's very little work left to do to make it good enough for a library: but such textbooks do not exist in research mathematics.)
> Granted their goal was not so much speed as it was elegance,
Do not underestimate the necessity of mathematical elegance. Mathematical notation is a tool powerful enough to teach machines to think: it is essential to make these tools elegant, or you will not be able to communicate your insight to your colleagues, and certainly not the next generation. Treating the goal of mathematics as "prove the most theorems as fast as possible" is hacking off the lower branches we should be using to climb trees, simply to harvest their fruit.
¹: Anyone familiar with my HN comment history will know that I keep banging on about "cannot in principle" and "there are deep theoretical reasons that an LLM can never". I'm not doing that here: I don't know a reason that LLMs can't produce elegant mathematical abstractions – probably because I don't understand mathematics deeply enough. "LLMs can't do this" is purely an empirical observation. (Believe me, I've read a lot of LLM-generated formal mathematics: it is invariably garbage. I just don't know why.)
(Sorry for the long post, but yours brought me thinking about a bunch of different aspects.)
First of all, I did not mean to downplay elegance at all. I agree that elegance is very important and that math is very much about trying to find elegant ways to think about various problems and phenomena. It also makes math feel more human and art-like, as elegance is not completely objective. And I also agree that LLMs do not seem to currently have consistent mathematical taste. I find they often do quite ugly or unoptimal proofs, although sometimes they also surprise me with a more elegant one than what I had in mind myself. And when we pass from arguments to choosing good definitions or seeing the big picture they are often much worse. Finally, formalization efforts such as Mathlib are very interesting from the elegance point of view. I'd actually be interested to see whether it would be possible to do lecture notes or textbooks based on Mathlib, written in standard math prose so that wider crowd of mathematicians might benefit from the insights that people had while formalizing.
However, as a research mathematician, I think we might now be approaching the situation where I can do my research pretty much as I usually do it, but at the same time in parallel have formalized proofs for the lemmas and theorems. These formalized versions are at least at the moment not going to have pretty proofs, and the proofs the LLM comes up with might even be different from what I'm writing in the paper (but probably in practice not very different if I'm formalizing every lemma). Still, if this can be done quickly enough, I think the result could be net positive even if the formalizations never leave my local hard drive: I will have confidence that I did not miss an edge case in the statements, where usually double-checking these things is actually a very time-consuming part of writing a paper. Thus I might be able to produce papers with less mistakes (usually non-important ones but they do happen). In this sort of workflow speed matters, and if you need a particular prerequisite theorem from the end of a textbook, you'd rather do it faster than half the reading speed (that's impressive by the way, and I do not mean this sarcastically!).
Returning a bit to the topic of elegance, I'd also like to claim that the elegance of arguments is probably at least as important as the elegance of definitions. And if you find an elegant argument, later on that might serve as a basis of a definition. There might also be some difference in how well this works out in practice in different fields. At least historically people in analysis (like myself) are happy to repeat known arguments in slightly different settings. It could be hard to make a version that works in every setting because different sets of assumptions could allow for a similar argument to work. Or it could also be easier to just remember the actual technique rather than trying to give it some jargonish name. Anyway, as I said above, I think LLMs are a bit better with arguments than definitions, so some elegance might be retained and perhaps you can later refactor to use more elegant definitions as well. (Hmm, a random idle thought, but a refactor from arguments to specific theorems could be in some sense similar as going from an untyped or not-explicitly-typed programming language to a typed one so there might be a coding analogue here as well.)
Finally, thanks for bringing up the limitations of LLMs. I also feel that LLMs are probably not currently able to really go beyond their training data, producing new theories with truly novel arguments or definitions. I'm skeptical that we will see a proof of the Riemann hypothesis in near future just drop from an LLM (human utilizing an LLM could be a bit of a different story, but I'm not a number theorist and have no idea whether anyone in the field has any plausible attack vectors currently). They are getting very good at combining and rephrasing existing stuff, however.