Granularity-Adaptive Proof Presentation
  When mathematicians present proofs they usually adapt their explanations to
their didactic goals and to the (assumed) knowledge of their addressees. Modern
automated theorem provers, in contrast, present proofs usually at a fixed level
of detail (also called granularity). Often these presentations are neither
intended nor suitable for human use. A challenge therefore is to develop user-
and goal-adaptive proof presentation techniques that obey common mathematical
practice. We present a flexible and adaptive approach to proof presentation
that exploits machine learning techniques to extract a model of the specific
granularity of proof examples and employs this model for the automated
generation of further proofs at an adapted level of granularity.
