Example-driven machine-human collaboration in mathematics

在最近一项关于数学家谈论什么的研究中，我们发现例子构成了最大的一个类别。这些可以是一个概念的例子，比如自然数的集合是一个群的例子，数字3、4和5是一个毕达哥拉斯三元组的例子，或者是一个猜想的支持或反例，比如1和3是两个奇数的和是奇数的猜想的反例。研究发现，在对话的不同阶段，使用例子的原因不同，例如，为了理解一个猜想，为了测试它，或者扩展它。作为数学中使用实例的一个例子，考虑下面的对话，摘自一个解决猜想的在线论坛：“如果这些点形成一个凸多边形，这很容易。[匿名者- 2011年7月19日晚上8:08]“是的。如果有一个点不在凸包上，我们能做到吗？“假设有四个点：一个等边三角形，然后在三角形的中心有一个点。没有三个点是共线的。在我看来，风车的中心点不能再用一次了！一旦它碰到一个角点，它就会无限循环地穿过这些角，永远不会回到中心点。我一定是漏掉了什么……“这不是真的——它会在三角形的中心和每个顶点之间交替。“[Joe - 2011年7月19日晚上8:21]在这里，我们看到人们提出简单的例子来支持一个猜想，并提出和讨论其他例子作为潜在的问题。在这个项目中，我们将建立在我们对数学实例使用的调查基础上，并采用第三方模型生成器，设计和构建一个系统，该系统可以通过以下方式与在线数学对话接口：1。手动和自动引入对话规则，以确定在对话中何时引入示例是合适的。发现一个例子在某一点上将扮演什么角色的论证模式。手动和自动诱导公理集作为输入到模型生成器。从模型生成器中选择有用的输出示例。向示例中添加上下文信息，例如它是否是对先前评论的回复，或者为什么这个示例在这一点上感兴趣。以对其他（人类）参与者有用的方式将示例与上下文信息一起添加到对话中。这将汇集理论论证，自动推理系统，和民族志，认知和哲学的研究，人们如何做数学。原型系统将通过在实时数学对话中运行来进行评估，并通过各种措施来观察数学家是否认为它有用，以及他们是否准备好与它直接交互。此外，在项目期间，我们将建立一个新的和广泛的潜在研究用户网络，以确定这种跨学科工作可能采取的进一步方向。

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.