Hierarchical structured mathematical proofs (my readings #2)

Today I stumbled upon a thoughtful paper by Leslie Lamport (someone may know him as the creator of LaTex) concerning a stronger method of writing mathematical proofs. Hierarchical structured proofs rely on a more rigorous frame which makes undoubtedly clear each step of the proof: a winning strategy for both educational and research purposes.

I found the reasons behind his work deeply shareable, and the final part of the article made me wonder about a future where mathematics and CS will be more connected within the realm of formal proof checking and computer-aided proofs. An easier way of writing proofs it's a necessary step toward a more sound mathematical research and thus a more sound mathematical approach to problems.

How to Write a 21st century proof by Leslie Lamport