Are We Stuck with Lean?

> 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 (not-quite-naïve) brute-force. Writes awful proofs (even if half a minute of staring reveals elegant concepts behind it), and can take a very long time to run 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, and will happily take you at your word. 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` and the editors will desk-reject it, but sledgehammer will still work fine (provided you put this before the things that require it: that's a mistake you only make once).

One thing to note: if this theorem isn't true, then Sledgehammer is prone to helpfully exploiting the principle of explosion to prove everything else for you, even other things that are not true. You can usually spot this at a glance, if it's dragging in unrelated theorems.

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

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

Yeah, we call that category theory. The big downside of Isabelle/HOL is that it can't do category theory, because it can't quantify over types: each "argument" has to be written out explicitly, generic over a large (usually infinite) family of use-cases, but not all of them in the way that a dependently-typed logic like Lean can.

But this limitation does make the automation more powerful, so that's actually a good thing for your use-case. I don't understand enough to know how it makes it more powerful, but I imagine it's something like "narrowing the search lets you search deeper". Lean's (currently, and perhaps inherently, inferior) version of sledgehammer has a module that tries to translate Lean expressions into HOL expressions, so it can use some of the techniques available to Isabelle/HOL's sledgehammer. (Some of the Isabelle people have joked that instead of using LLMs, Lean should just bundle a copy of Isabelle/HOL – and while obviously this wouldn't work, it might genuinely work better than LLMs for most use-cases.)

> 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! And it'd have done exactly the same for a lesser-known theorem, provided that the theorem was known to Isabelle.) LLMs (usually (when they succeed)) give you answers, and then do a post-hoc search for where the answers might have come from.

¹: The scare quotes around "just" are doing a lot of heavy lifting. Jasmin Blanchette is a clear communicator, so most Sledgehammer articles are accessible to non-experts: you may find Sledgehammering Without ATPs (https://doi.org/10.4230/LIPIcs.ITP.2025.38) or Exploiting Instantiations from Paramodulation Proofs in Isabelle/HOL (https://arxiv.org/abs/2508.20738) interesting reading. Or Redirecting Proofs by Contradiction (https://isabelle.in.tum.de/~blanchet/redirect.pdf), which describes a much older version of Sledgehammer and is rather technically-dense, but has some interesting observations about human versus computer mathematics.

I don't see what the issue is. Isn't the entire point of LLMs that we can easily translate between languages? What better way to cross check the correctness of a proof than to run it on several different systems simultaneously.

You are right, and the first version of my comment had exactly all this hedging (though less educated and sophisticated than your version).

When I said 'Haskell', I really meant 'vanilla Haskell a sane person might want to write'. Similar to how C++'s type system is fully Turing complete, but you shouldn't use it that way.

No programming language will ever be perfect. But it's still better for everyone to focus on improving one language than to recreate the same ideas across dozens of different languages, like a Tower of Babel of duplicated effort.

That's a bad analogy. LEAN is a leading bleeding edge proof verification tool.