Information Technology Reference
In-Depth Information
that a proof has actually been given, i.e. when a consensus on the validity of the
purported proof is reached among the relevant community of agents. This marks the
termination of the sequence of proof-events (the history of the proof). Otherwise,
the proof is not considered valid and the relevant community remains in a state of
indecision. Therefore, the community of relevant agents is the ultimate truth-maker
of the (sequences of) proof-events.
Thus the truth of the proof is ultimately declared by the relevant mathematical
community, which is competent enough to check the proof. However, in the case of
computer-generated proofs, their validation by humans can be practically impossible,
since no human or group of humans is capable of checking a huge number of proof
steps. What can be considered as validation in such a case is the validation of the
correctness of the theorem-prover itself (as a program). Therefore, in this case, vali-
dating the program can guarantee that all possible proofs generated by this software
tool have been “validated”. One way or the other, either by human or by automated
means, the final output of the validation needs the recognition or consensus of the
mathematical community to be regarded as true. This marks the termination of the
sequence of proof-events at this particular time.
18.4 Web-Based Mathematical Problem-Solving as Proof-Event
The conceptual framework outlined above is adequate to describe Web-based mathe-
matical problem solving as proof-events as is practiced in the Kumo [
7
] and Polymath
projects [
8
,
17
].
Web-based proving appears to be a novel kind of proving practice, having new
important features. First, it is characterized by a
change of the communication
medium
: the Web serves as both an information source (a repository of informa-
tion, ideas and methods available) and a communication medium (creating global
interest-based communities). Web-based mathematical problem-solving is
open
to
all, and communication is transformed from one-to-one or one-to-many into
many-
to-many
. Second, the use of the Web as a medium of communication between agents
opens new possibilities of interactivity between the agents involved in a proof-event.
The agents are located in a
virtual
environment, when for instance human agents
interact with software entities through the Internet. For example, agents could inter-
act through a
blog
, in the case of Polymath project, or in a more sophisticated way,
through
proofweb
sites (displayed as
proof pages
or
Tatami pages
) in the case of
Kumo. This facilitates the formation of new metaphors for information visualization
and proof representation. Interactivity also enables the formed group of agents to
collaborate on the problem by behaving like a goal-directed agent system, in which
agents enact interchangeably both roles of prover and interpreter. This results in
astonishing intensification and speed of the mathematical problem-solving activity.
Interactivity in Web-based mathematical problem-solving, as practiced, for
instance, in the Polymath project, enables the use of a group problem-solving tech-
nique known as brainstorming [
13
]; in particular, (asynchronous) computer-mediated
Search WWH ::
Custom Search