Photo by Hannah Gleg 
Project DescriptionIn his book Proofs and Refutations, Lakatos identifies seven methods by which mathematical discovery and justification can occur. These methods suggest ways in which concept definitions, conjectures and proofs gradually evolve via interaction between mathematicians. Different mathematicians may have different interpretations of a conjecture, examples or counterexamples of it, and beliefs regarding its value or theoremhood. Through discussion, concepts are refined and conjectures and proofs modified. For instance, when a counterexample is found, one might look for general properties which make it fail a conjecture, and then modify the conjecture by excluding that type of counterexample (piecemeal exclusion). Alternatively, one might generalise from the positives and then limit the conjecture to examples of that type (strategic withdrawal). Another reaction might be to deny that the object is a counterexample on the grounds that the conjecture refers to objects of a different type (monster barring). Given a faulty proof, a counterexample may be used to highlight areas of weakness in the proof, and to either modify the proof or the conjecture which it purports to prove (lemma incorporation).Our main aim was to provide a computational reading of Lakatos's theory, by interpreting it as a series of algorithms and implementing these algorithms as a computer program. We hypothesised that this is (a) possible, and (b) useful. In order to test our hypotheses we developed a system within which we implemented his methods: HRL. This is a multiagent automated theory formation programme in which each agent has a copy of Colton's theory formation system HR, which can form concepts and make conjectures which empirically hold for the objects of interest supplied. The conjectures are communicated to the other agents, who send counterexamples if they have them. Agents then use Lakatos's methods to suggest modifications to conjectures, concept definitions and proofs.

PeopleThe following people were involved with the project:Alan Smaill  supervisor (A.Smaill _AT_ ed.ac.uk) John Lee  cosupervisor (J.Lee _AT_ ed.ac.uk) Simon Colton  cosupervisor (sgc _AT_ doc.ic.ac.uk) Alison Pease  PhD student (A.Pease _AT_ sms.ed.ac.uk) FundingThis work was supported by EPSRC grant GR/M45030We completed the project in June 2007. For further details, see my PhD thesis. 