> 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.

If you were using Isabelle/HOL, then (depending on field) you could already have had this. Sledgehammer is pretty powerful, even though it's "just" SAT solvers plus brute-force. Writes awful proofs, and can take a very long time if you don't have sensible intermediate lemmas (although you'll be writing those anyway, in the course of your work), but if you start at the top of the page and work down, writing "try" in place of every proof, you'll get proofs (or counterexamples) of nearly everything, without putting in any extra work. (This is pre-LLM technology, to be clear: they just have a terrible marketing department.)

There's currently a UI issue where you have to accept the proofs in reverse order (bottom to top), otherwise it goes "oh, something changed!" and wipes the attempts it was making for the later proofs; but that shouldn't be too hard to fix with a non-local cache – and in the meantime, it's quite a minor quirk. On a researcher's laptop (i.e., one considerably more powerful than mine!), it's rare that sledgehammer finds a proof slower than it takes to type out the statement of the next theorem, and the "try" keyword changes background colour to let you know when it's done.

You'll notice I said "sensible intermediate lemmas". You might need to recalibrate your notion of elegance slightly for this, if you want to get fast proofs out the other end – but sledgehammer can work with even totally backwards lemmas like "∀list. list = hd list ## tl list": it'll just use a general-purpose solver rather than a special-purpose one, and so be a lot slower to find proofs. In practice, this is not an issue: it's an easier, more explicable skill than prompt engineering, and Isabelle will mostly just work around you if you do it wrong.

> 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, […])

Note that this is my mathematics reading speed, not my English reading speed. It might not be as impressive as you think. The number of times I've had to go back and re-read four pages because I misunderstood a basic concept…

Well, if I were formalising for the sake of assisting my research, rather than for the joy of formalisation (which, honestly, isn't all that: Isabelle's better than Lean, but it's far from nice), and I just needed a result from the end of a textbook, I'd be very tempted to write:

  theorem final_theorem: ‹statement of theorem›
    sorry  ― ‹TODO: Proven in textbook reference, page 189.›

Isabelle doesn't care. You won't be able to publish it in the Archive of Formal Proofs (a journal of formalised mathematics) because `thm_oracles final_theorem` will say `skip_proof`, but sledgehammer will still work fine (provided you put this before the things that require it: that's a mistake you only make once).

> 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.

Yup! And sometimes different arguments motivate different definitions, and then you end up with a graph of "definition A is easier to prove from definition B than the other way around", which either resolves into a "definition I is the best weak definition for introduction, and definition D is the best strong definition for destruction/elimination", or a circle of equally-valid definitions. (Sadly, I've only encountered the latter in textbooks: never in my own research, however often I've believed I have. But I'm holding out hope!)

> I think LLMs are a bit better with arguments than definitions

So's Isabelle's sledgehammer. Try it? (Again, depending on which field you work in: some things just aren't formalised at all in Isabelle/HOL, so you can't really use them, although a surprising amount is. Given more information, I can give better advice.)

> I also feel that LLMs are probably not currently able to really go beyond their training data, […] They are getting very good at combining and rephrasing existing stuff, however.

I'm concerned that this will lead to increased plagiarism. When Isabelle finds a proof, it tells you where it got it. (That's actually how I learned about the Cantor–Schröder–Bernstein theorem, which finally convinced me that what I was trying to prove was independent of ZF: it told me the name of this theorem, when solving a problem that I didn't think was deeply related to the axiom of choice. All pre-LLM technology, mind!) LLMs (usually (when they succeed)) give you answers, and then do a post-hoc search for where the answers might have come from.

Are We Stuck with Lean?