Donald Knuth's literate computing could be an example to follow:
combine lean prove language with inline English human language that explains it.
Then, Lean files can be fed into Lean to check the proof, and LaTeX files
can be fed into LaTeX to produce the book that explains it all to us mere mortals.
combine lean prove language with inline English human language that explains it. Then, Lean files can be fed into Lean to check the proof, and LaTeX files can be fed into LaTeX to produce the book that explains it all to us mere mortals.