Qualitative Aspects of Mathematical Proofs - the Case of Granularity

mathematics (Thomas Hales's "Flyspeck" project, for example) and engineering
(like the "Verisoft" project), the main concern is the question of whether a
proof exists for a formal problem.

But in many application areas of artificial intelligence (like intelligent
tutoring), other aspects of proofs become relevant, namely the aspects of
granularity and relevance of the proof steps. Here, "granularity"
designates the "size" of a proof step in terms of abstraction, cognitive
effort and its linguistic representation.

In the scope of the thesis, the challenging task of systematically
"evaluating" the granularity of proof steps via methods from automated
theorem proving has been investigated.

As a part of the work, empirical data has been collected in an exploratory
study in the "Wizard of Oz" paradigm. During the study, the subjects had to
solve mathematical proofs collaboratively with an "intelligent tutoring
system". The collected corpus of data serves to identify the role of
granularity in the judgments of the "wizard". Furthermore, possible methods
to evaluate the formalized proof steps with respect to granularity were
investigated, which involves the study of human-oriented calculi, the
implementation of proof methods in a "cognitively plausible" calculus, the
development of a framework for the automatic evaluation of proof steps, as
well as a first evaluation with proof steps from the corpus.

The talk will provide an overview of the issue of granularity in
mathematical proofs, the design of the empirical study and some first
observations, as well as the techniques developed and applied as part of
the thesis.