Collective Discovery Events: Web-Based Mathematical Problem-Solving with Codelets - Computational Creativity Research: Towards Creative Machines - page 367

or communication of a narrative that is addressed to particular social groups, who
are assumed to have particular skills and expertise, enabling them to perceive the
narrative and formulate a conclusion on it. Proof-events are not confined necessarily
to communication of mathematical truths, since a proof-event may concern the pre-
sentation of an incomplete proof, a false proof, or a proofless, intuitive exposition of
ideas on a particular problem.
Following Goguen's idea, proof-events presuppose the involvement of at least
two types of agent: a prover , which can be a human or a machine or a combination
of them (in the case of hybrid proving), and an interpreter , who generally can be a
human (or group of humans) or a machine (or group of machines) or a combination
of them. Both types of agent are situated in an environment that might be a real
physical one, like a material world inhabited by various kinds of things (objects), or
a virtual ,ora simulated one, when for instance human agents interact with physical
tools and software entities or the Internet. An agent is equipped with past background
knowledge and past learning experience.
A human prover may experience an insight (intention) that something in mathe-
matics is true and produce an item (choosing some semiotic code) to encode their
experience. This item may be not a complete proof, but an outline of a proof or even
a conjecture. This initiates a proof-event. The prover may feel so confident in the
truth of their experience, that they may decide to present the produced item publicly,
expecting that a potential reader (interpreter) will be persuaded easily in the truth
of their experience and will succeed in understanding (decoding) it, as the prover
understands it. Thus, the time of public communication of the item can be considered
as an ending point of a proof-event. In the case of a machine, this is the time that the
machine halts and produces an output.
Thus, agents enact different roles , according to their type. The roles enacted by
agents determine their tasks with respect to a specified problem (defined by certain
conditions ). The task of a prover is to set a problemand develop an argument that aims
at providing support or even a proof to a given problem; the task of an interpreter is to
understand or interpret or verify a suggested argument or proof. The implementation
of this task may involve the use of a computer program to verify a suggested proof,
or to check certain special cases of a suggested proof, or to find a gap in a suggested
proof or cross-check the proof. Moreover, the interpreter may undertake the task to
fill the gap in the proof by advancing a new proof, or to invent a counterexample
that would ultimately refute the proof, or reformulate the gap as a new problem. In
these cases, the interpreter enacts as prover, rather than interpreter. The tasks of the
prover and the interpreter have different goals and can be realized in different proof-
events that are successive in time forming a sequence of proof-events . A sequence
of proof-events evolves in time with reference to a fixed underlying problem and
represents the history of a proof . An agent can freely change roles in the course of
history and enact as prover at a certain time and as interpreter at another time of
a sequence of proof-events. Moreover, the definition of concepts and standards of
rigor are not invariant during the unfolding of a sequence of proof-events, since the
task of an interpreter includes possible gap-filling operations that may be fulfilled