Yup, that's mostly a factor of using declarative proofs rather than lists of proof "tactics" based on an entirely opaque proof state (that can only be reconstructed and understood by replaying them in the proof system). You'd find these proofs in systems like Mizar or Isar (a declarative framework that's part of Isabelle). Systems like Lean and Coq/Rocq do support structured proofs that can act as a minimal step towards declarativity but are not nearly as readable as actual declarative proofs.