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

a sentence—destroys the perceived syntactic structure and necessitates a re-reading
of the phrase. Indeed, with a fresh set of codelets working at the syntactic level from
scratch, the word “meaning” can be seen as a participle, in which case the pronoun
“it” cannot refer to “meaning” but to something else prior to the given phrase. (For
example, the phrase could be part of this sentence: “He claimed that the islet did not
exist, actually meaning that he failed to discover it.”)
Now take the case of collaborative theorem proving. A person engaged in solving
a particular task toward the completion of a proof can be thought of as a codelet. The
task could be proposed by a supervising codelet (some person, but with a somewhat
wider view of the project), and could be taken by a pool of people who have volun-
teered their services and availability to the proving project, as long as they feel that
the task is suitable for their abilities. Similarly, a person working on a codelet could
assign sub-tasks as other codelets, of simpler nature and of an ever-narrower view
and scope, which can be taken by less qualified or less specialized proving agents.
At the highest level could stand a person of qualified knowledge who gave the initial
broad strokes, i.e., decided the highest-level tasks and placed them in the “codelet
pool” to be undertaken by qualified agents. The tacit assumption is that perhaps in
this way proofs of greater complexity can be achieved than is possible by the faculties
of a single person-prover. In the rest of this chapter we shall examine this idea more
thoroughly.
18.3 Mathematical Problem-Solving as Proof-Event
Goguen introduced the concept of proof-event in an attempt to formulate a wider
viewpoint on proof, designed to incorporate traditional mathematical proofs (both
constructive and non-constructive ones), but also non-mathematical proofs (apodic-
tic, dialectical, ontological, etc.) as well as new kinds of proving practice, such as
computer proofs and proof steps.
Mathematicians talk of “proofs” as real things. But the only things that can actually happen
in the real world are proof-events, or provings, which are actual experiences, each occurring
at a particular time and place, and involving particular people, who have particular skills as
members of an appropriate mathematical community....
A proof-event minimally involves a person having the relevant background and interest, and
some mediating physical objects, such as spoken words, gestures, hand written formulae,
3D models, printed words, diagrams, or formulae (we exclude private, purely mental proof-
events...). None of these mediating signs can be a 'proof' in itself, because it must be
interpreted in order to come alive as a proof-event? we will call them proof objects . Proof
interpretation often requires constructing intermediate proof objects and/or clarifying or
correcting existing proof objects. The minimal case of a single prover is perhaps the most
common, but it is difficult to study, and moreover, groups of two or more provers discussing
proofs are surprisingly common (Goguen [ 6 ]).
From this point of view, a proof-event is a social event: it takes place at a cer-
tain location and lasts for some time interval; it also involves a public presentation