Collaborative Theorem Proving

Source: De Gruyter.com, 2015

Another project of distributed cooperative proving was initiated by Timothy Gowers [G], a Fields Medal-winner Cambridge mathematician, in 2009. He called on the community in his blog to find a new, more intelligible, solution of a special case of the density Hales-Jewett theorem [DHJ] (Hales and Jewett 1963).

This marks the beginning of a proof-event, i.e. the system starts from the state 〈 〉 G DHJ , . Each agent Ai , who joined the system, had to use the comment function of Gowers’s’ blog to communicate insights, ideas, approaches, pieces of proof, etc. (whenever acted as prover), or to comment, correct, or reject ideas proposed by other agents (whenever acted as interpreter). Each attempt has the features of a brainstorming session and represents by itself a proof-event in a sequence of proof-events. The evolution of the sequence in time is represented in the “history” kept by the medium (the blog)18. The attempts (proof-events) were developed in time along two main sequences of proof-events in the respective blogs of Gowers and Terence Tao, another winner of the Fields Medal.

Both sequences produced outputs that were finally evaluated as actual proofs of the problem and were published under the pseudonym “Polymath” (2009, 2010a, 2010b), which denotes a collective author19

The Polymath project was the first real experiment of collective Web-based proving carried out by agents of varied knowledge background and expertise skills, who worked as a goal-directed system. A blog was used to create an interest-based community of agents, whose exchange and cross-fertilization of ideas amplified collective creative thinking that led to a fast solution of the problem.

Related Resource: Polymath Timeline, Apr 2009

Advertisements

Leave a Reply

Fill in your details below or click an icon to log in:

WordPress.com Logo

You are commenting using your WordPress.com account. Log Out / Change )

Twitter picture

You are commenting using your Twitter account. Log Out / Change )

Facebook photo

You are commenting using your Facebook account. Log Out / Change )

Google+ photo

You are commenting using your Google+ account. Log Out / Change )

Connecting to %s