Eliciting implicit assumptions of proofs in the MIZAR Mathematical Library by property omission

TL;DR

This paper presents a method to identify implicit assumptions about properties of functions and relations in formal proofs within the MIZAR Mathematical Library, aiming to clarify background knowledge used implicitly during proof formalization.

Contribution

It introduces an approach to elicit implicit property assumptions in formal proofs, enhancing understanding of background knowledge in interactive theorem proving.

Findings

Successfully identified implicit property assumptions in MIZAR proofs

Improved transparency of background knowledge in formal proof libraries

Facilitated better understanding of proof dependencies and assumptions

Abstract

When formalizing proofs with interactive theorem provers, it often happens that extra background knowledge (declarative or procedural) about mathematical concepts is employed without the formalizer explicitly invoking it, to help the formalizer focus on the relevant details of the proof. In the contexts of producing and studying a formalized mathematical argument, such mechanisms are clearly valuable. But we may not always wish to suppress background knowledge. For certain purposes, it is important to know, as far as possible, precisely what background knowledge was implicitly employed in a formal proof. In this note we describe an experiment conducted on the MIZAR Mathematical Library of formal mathematical proofs to elicit one such class of implicitly employed background knowledge: properties of functions and relations (e.g., commutativity, asymmetry, etc.).