Example-driven machine-human collaboration in mathematics

点击翻译按钮获取中文摘要

In a recent study of what mathematicians talk about, we found that examples form the biggest single category. These may be examples of a concept, such as the set of natural numbers being an example of a group, and the numbers 3, 4, and 5 an example of a Pythagorean triple, or supporting or counterexamples to a conjecture, such as 1 and 3 being a counterexample to the conjecture that the sum of two odd integers is odd. The study found that examples are used for different reasons at different points in a conversation, for instance to understand a conjecture, to test it, or extend it.As an example of example-use in mathematics, consider the following conversation, taken from an online forum for solving a conjecture:"If the points form a convex polygon, it is easy.'' [Anonymous - July 19, 2011 @ 8:08 pm]"Yes. Can we do it if there is a single point not on the convex hull of the points?'' [Thomas H - July 19, 2011 @ 8:09 pm]"Say there are four points: an equilateral triangle, and then one point in the center of the triangle. No three points are collinear. It seems to me that the windmill can not use the center point more than once! As soon as it hits one of the corner points, it will cycle indefinitely through the corners and never return to the center point. I must be missing something here...'' [Jerzy - July 19, 2011 @ 8:17 pm]"This isn't true - it will alternate between the centre and each vertex of the triangle.'' [Joe - July 19, 2011 @ 8:21 pm]Here we see people raising simple examples in support of a conjecture, and proposing and discussing other examples as potential problems.In this project we will build on our investigations into example-use in mathematics, and employ third party model generators, to design and build a system which can interface to online mathematical conversations by:1. Manually and automatically inducing dialogue rules to determine when in a conversation it would be appropriate to introduce an example.2. Discovering argument patterns as to what role an example will play at a given point.3. Manually and automatically inducing sets of axioms as input to the model generator.4. Selecting useful output examples from the model generator.5. Adding contextual information to the examples such as whether it is a reply to a previous comment or the reason why this example is of interest at this point.6. Adding the examples alongside the contextual information into a conversation in a way which is useful to other (human) participants.This will draw together theories of argumentation, automated reasoning systems, and ethnographical, cognitive and philosophical studies of how people do mathematics. The prototype system will be evaluated by running it on mathematical conversations in real-time, and seeing, by a variety of measures, whether mathematicians regard it as useful, and whether they are prepared to interact directly with it.Furthermore, over the duration of the project, we will build a new and broad network of potential research users, in order to determine further directions which such inter-disciplinary work may take.