Isabelle proving environment implements this idea since at least 2005 when I started using it. One can interleave formal proofs and informal commentary in a theory file and one of the artifacts is a "proof document" that is a result of LaTeX processing of the file. Other options exist as well where the file is exported to HTML with hyperlinks to theorems and definitions referenced in a proof. There are also custom HTML renderers (since 2008) where a reader can expand parts of the structured proof when they want to see more details.
Agda 1 (more specifically, the included UI program known as Alfa) implemented an automated translation from formal proof to natural language, driven via Grammatical Framework. This requires writing snippets of code to translate every single part of the formal language to its natural language equivalents, at varying levels of verboseness - for example, (add ab) could become "a + b", "the addition of a and b", "adding b to a" and so on. Similar for proof steps such as "We proceed by induction on n", properties such as "is commutative" etc. The idea gets reimplemented every now and then, in a variety of systems. Of course the most compelling feature is being able to "expand out" proof steps to any desired level of detail.
