Granularity-Adaptive Proof Presentation

TL;DR

This paper introduces a machine learning-based approach to adapt proof presentations in automated theorem proving, making them more suitable for human understanding by adjusting the level of detail according to context and user needs.

Contribution

It proposes a novel adaptive proof presentation method that models proof granularity and generates proofs tailored to specific didactic goals and user knowledge.

Findings

Successfully models proof granularity using machine learning

Generates proof presentations at adaptable levels of detail

Aligns automated proofs with human mathematical practice

Abstract

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.