A Method for Adapting Granularity of Mathematical Proofs using Metamath

Understanding mathematical proofs is often not an easy task, especially in the first introductions. One of the determining factors in understanding a mathematical proof is the level of detail at which it is presented. In order to help resolve this issue, this article proposes a method for adapting the granularity in which a mathematical proof is presented. It makes use of structured theorems in metamath language as a basis, which allows access to the details of each step used in the proof. To describe the method, an example is presented with a simple theorem involving numerical sets.