Isabelle comes with a proof language layer Isar, designed specifically for readability: https://isabelle.in.tum.de/Isar/ https://isabelle.in.tum.de/Isar/ The s

Isabelle comes with a proof language layer Isar, designed specifically for readability: https://isabelle.in.tum.de/Isar/ https://isabelle.in.tum.de/Isar/ The structure of Isar proofs then more closely resemble a traditional mathematical proof, with a formalisation close to natural language. You can see the example from Wikipedia: https://en.wikipedia.org/wiki/Isabelle_(proof_assistant) https://en.wikipedia.org/wiki/Isabelle_(proof_assistant) As you can see, the overall structure of the proof is clearer, and you have less dependency of seeing the proof state to understand the proof. The downside to Isabelle is that it introduces a dual syntax, with certain sections written in quotes. There's more to learn syntax and concept wise, but I think it's worth the extra effort for a clearer proof. EDIT: Linked to Wikipedia page for formatting.