Workshop on
Mathematically Intelligent Proof Search
MIPS 2010

Paris, France, 10th July 2010

The workshop on Mathematically Intelligent Proof Search explores the relationship between mathematical theory development and proof construction. It aims most directly at taking steps towards a deeper understanding of this relationship in both informal and formal contexts, but has the central, long-term goal of bringing these two contexts closer together in a systematic way. This would pave the way for having machines analyze mathematical texts and uncover leading ideas or heuristics for parts of mathematics.

In either context, theory development and proof construction are deeply connected: the choice of a language, expanded by definitions, and of a corresponding inference mechanism correlates with how effectively proofs can be obtained and how well mathematical arguments can be communicated. Thus languages can range from mathematical vernaculars that are close to natural languages to purely formal ones; inference mechanisms can structure arguments conceptually but may also be based on automated proof procedures that are mathematically intelligent.

MIPS will bring together researchers from Computer Science, Linguistics, Mathematics and Philosophy who are interested in the whole subject or parts of it, in order to get an overview of the state of the art, present original results and discuss directions for future research:

The scope of MIPS thus includes topics such as

  • formalization and automated proof search for mathematical theories:
    • domains of specific interests are set theory and geometry
    • interactive verification and automated proof search
    • alternative formalizations and their adaptive selection
  • analysis and generation of mathematical texts
    • natural language vs. controlled natural language
    • domain specific vs. generic lexika text analysis
    • textlinguistic aspects of mathematical texts
    • cognitive aspects of the conceptualization and representation of mathematical texts
    • adaptive document generation styles

with practical applications for
  • authoring of mathematical texts
  • verification of mathematical documents
  • dynamic proof tutoring in mathematics

We encourage researchers working at points of contact among these fields to share their views, work, or results by submitting a title and abstract or short paper (2-5 pages in PDF format) and taking part in the workshop. Please submit your work via EasyChair Any questions you may have about the workshop should be send to

Submission of title and abstracts:
June 18, 2010
Notification of acceptance:
June 24, 2010

The accepted work should be presented at the workshop, which will be a mixture of invited and accepted presentations. The abstracts/short papers of the accepted and invited presentations will be collected in informal proceedings and made available at the workshop.