Comment by robinzfc

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.