Post #2798886

Why is there no Isar-like structured proof mode in Lean, like there is for Isabelle? In https://leanprover.zulipchat.com/#narrow/channel/270676-lean4/topic/Thoughts.20about.20Isar.20and.20Lean/near/591162685 I offer two answers: 1. There is now (AI-assistet proof of concept): https://github.com/nomeata/lean-lisar, proving that it's certainly well possible. 2. It doesn’t seem to be needed that much. (Assume it were. Someone would have built it if it is possible. And from the point above it follows that it is possible.) #leanProver #isabelle #itp