“Oh dear, better use Lean then.” — was the first response by an Isabelle core maintainer when I asked how to use Isabelle/HOL with VS Code / GitHub Copilot. … So, should one?
I’ve been an Isabelle/HOL user for 15 years, finished several projects in it, and taught it to many students and colleagues. But maybe it’s time to jump on the Lean train?
In 2021, I was at a similar crossroads. Should I formalize my PhD research in Lean or Isabelle? Lean was just upgrading from 3 to 4, disregarding structured proofs. While I like functional programming and the Curry–Howard correspondence, I don’t think the way Lean (and Rocq) double down on it helps readability. Finally, I opted for Isabelle because of its maintainable proof syntax and clarity.
Since then, Lean has continued to take off. That’s annoying for experts, as the booming community means that people keep reinventing the wheel and producing a lot of not-so-elegant stuff. Isabelle on the other hand is as walled a garden as an open source project can be. (No GitHub repo, special versioning system and tech stack. Giant barriers against drive-by pull requests and issue reports!)
The cited core maintainer is known for his particular style of communication on the mailing list—so, one should not take the offensiveness of the quoted sentence too seriously. But there’s something else about the attitude it reveals:
It seems that a maintainer writing a sentence like “Better use [our competition] then!” has already given up the fight for his system to be the one that people will use in the next decade. It tastes of seeing the writing on the wall and actively refusing to adapt to new trends, in order to not feel passive about it.
I might be totally wrong about all this. Maybe, it’s the right strategy to keep Isabelle on an island. But still, I can’t unsee the dynamic I think to see. And for me, the possibility to use a system in VS Code as well as maintainer attitude contribute to turning the scale on which system to use for my next 10000 lines of formalized math.
So, what do you think? Should one “better use Lean“? (Or Rocq? ;) Or re-learn pen-and-paper math? ;P )
