Rigorous formal proof is one of the key techniques in the natural sciences, engineering, and of course also in the formal sciences. Progress in automated reasoning increasingly enables computer systems to support, and even teach, users to conduct formal and mathematical proofs. A remarkable skill of mathematicians (and other proficient thinkers) is to create and represent proofs flexibly at various step sizes (such that proofs differ in their so-called proof granularity) as needed. This contributes to the effectiveness of human reasoners in searching, representing and communicating proofs. Computer-generated proofs, by contrast, typically differ from those produced by human reasoners with respect to the step sizes they employ and their flexibility to adjust them.
In view of this discrepancy, this work proposes a dedicated framework for modeling proof granularity. Within this framework, techniques are identified, developed and combined that serve to adapt computer-generated proofs to a step size suitable in a proof tutoring scenario. Norms for proof granularity are represented explicitly and can be inferred from classifications by human experts via machine learning techniques. The detection of suitable levels of granularity is applied to the automated assessment of proof exercises and in the generation of proof presentations. An empirical study investigates the automated learning of granularity judgments from experienced tutors.
