Proof events have been introduced by J. Goguen, as a means to semiotically study how mathematical proofs are built in practice. In short, proof attempts consist of a sequence of events unfolding in time, wherein some entities try to argue (possibly partially and/or non-formally and/or non-correctly) for a given claim and some entities validate the arguments.

The theory of institutions, grounded on category theory, describes logical systems as structures where models are related to some syntax via a satisfaction relation; this is optionally complemented by a proof system. Institutions can also formally describe translations between logics. Thus, they are suitable for studying elements of (the meaning of) proof events independently of the logic underlying every such event.

In the work to be presented, we first created an abstract and comprehensive formalisation of the notion of a mathematical problem, based on a formal institutional definition. The central idea is that every mathematical problem consists of four elements: a selection of an institution, a signature in the said institution, a set of sentences acting as premises, as well as sentence acting as the claim to be proved.

We have also sketched a range of proving (proof and disproof) objects that can incorporate proof attempts of varying levels of formality. We were then able to (re)define proving events and hypergraphs (dubbed fluents) of related proving events. This substrate enables modelling proof attempts that may span multiple logical systems, while also being able to study their semantic relationships.

Following this semantic viewpoint, we have also viewed problems and proving events argumentationally, focusing on how relations of support and attack can be defined in our framework, how support/attack may be deduced from the structure of problems and proving events, and how (joint) support can be thought of as a description of the notion of subproblem.