“KWARC was!”

Hypotheses: Mathematical Software needs MoC (well at least that was what I was going to show)

Evidence: I am referring to software that helps finding a proof, that supports the iterative process of adding proving steps and deleting them again, that is the tedious process of slowly approaching the proof in a notation one is satisfied with. I am not referring to theorem provers that proof lemma’s for us and fill in correct steps automatically nor to tools that help digitalizing already known or written proofs. The continuous revision and multiple revision require a permanent adaptation of previous written proofs steps, thus, respective software with management of change support is valuable for mathematicians.

Another feature: The tedious proving process is very different to the final proof or the later presentation of the process to other (in publications, books, slides, and even in discussions with other mathematicians). Thus, for reconstructing the actual proving process, the software can offer recording functionalities. This could be used by others (in particular students) to better understand the methodology of finding a proof and the heuristics used to require the proof (well, we can’t look in the mathematicians head; some iterations made not be entered but rather take place in the human mind or using pen and paper).

Revision/ Concerns: However, do mathematicians really want such a tool? It would be tedious to enter notations (and particularly to decide on a notation, thus, slowing down the actually thinking) and most likely mathematicians rather stick to their heads and paper. So we should rather ask: When do mathematicians use software? Where can software potentially ease up their life? Is this maybe rather after the finding of a proof; when it comes to the point the mathematicians want to share it with others, publish it; verify it (automatically)? So then we would not need software that supports the tedious, iterative phase of finding proofs … but rather software that supports the publication process (still then change management is useful, since notations/ text evolve - also when writing down an already completed proof) — and the learning experience (since young mathematicians need to learn how to proof).

So does learning software in mathematics make sense? Can it potentially ease up the learning experience? What can software do better/ more efficient/ and less costly then human specialists?

A final though: Mathematicians tend to collaborate to solve proofs (really?). And with the growing globalization, they can refer to modern technology to find potential collaborators and to communicate (do they?). Software can indeed be useful to provide the respective search facilities; communication channels; and digital working spaces (including change management). Software can thus influence and change mathematical practice by opening new spaces to do math (potentially interesting for particular young mathematicians).

James Davenport’s plea for providing more insights on the proof and how one got it done and … if a computer can’t solve it, is it really not provable. Shouldn’t it rather return “I can’t solve it”?

An interesting comment wrt. to the fact that William Farmer and Alan Bundy pointed me to, that is that the way mathematicians present and illustrate a proof (in publications, books, and even lectures) is not the way we actually retrieved the proof.

And it contributes to another interesting discussion, that is whether or not trusting and accepting automatically computed proofs (see the Flyspeck project).

There are multiple solution to a mathematical exercise:

• 8 ways for Three by One
• Different numbers of proving steps: see MKM: Specifying Strategies of Exercises

James Davenport gave a talk on mathematical units in OpenMath.

New to me was the discussion on whether and when CDs/ units/ notations are obsolete (e.g. out-of-date)

• OpenMath CD is obsolete if the definition in it are for archival purposes only.
• A unit is obsolete by formal change (e.g. liter_pre1964) and by usage.

Or to distinguish relative and absolute temperatures … for addition “abs”+”rel”=”abs” (not arith1-plus?) …

Units are also very interesting in making mathematical expressions more intuitive and context-dependent. Maybe: A renderer converting from 1.2 miles (English) to (ca.) 1,92 km (German) should also convert the units and thus needs to provide basic computations (e.g. from miles to km)?

William Farmer pointed me to an interesting point that I have so far not considered:

The way mathematicians present their work does not necessarily reflect the way the do math. These are two very different aspects of mathematical practice: The practice mathematicians (commonly) develop/ use to present their work and the practice they apply to do math (to solve mathematical problems). Consequently, limiting my analysis of practice to literature (mathematical results) and the included notation will not allow me to fully understand practice. Instead, I would need to observe and interview mathematicians to understand the way of doing math … or even start attending fundamentally math lectures (e.g. an abstract algebra course) and become a mathematician myself.

Mathematical text books worth while reading:

• Caculus (Michael Spivak)
• Algebra (Larry C. Grove)

In addition to mathematical text books, there is some (more philosophical) literature out there that can help to understand practice

• George Polya: How to solve it!
• Imre Lakatos: Proofs and Refutations
• Thomas S. Kuhn: The Structure of Scientific Revolutions
• Karl Popper: The Logic of Scientific Discovery
• Bettina Heintz: ie Innenwelt der Mathematik. Zur Kultur und Praxis einer beweisenden Disziplin

Some links, not all of them yet evaluated

• Listing Examples for the Methodology of Math citing P. Davis and R Hersh books “The mathematical experience” and “Descartes’ dream”.

Joseph Collins presented a Mathematical Model of the Physics Modeling Process and discussed the representation of Physics. He emphasized that semantics of objects vary in math and physics: For example,

• a physical field versus a mathematical field

See MKM 2008 proceedings “A mathematical type for physical variables”.

Johan Jeuring presented me their tool for incrementally solving exercises. The system provides a progress bar, feedback, and hints as well as verifies each step (so providing immediate feedback to the students). For each assignment one has to find a problem domain i.e. “simplifying fractions” and define the respective mathematical domain and a strategy for the type of problem.

For my work on mathematical practice this is extremely valuable, since their work observes and explicates ways of solving mathematical problems. In order to get the respective strategies they ask a mathematical specialist to explain them.

Very interesting approach. They take our notation-rendering approach on the level of documents, i.e. presentation markup is interpret wider and includes narrative presentation markup:

Plain text documents are first structured and verified; missing proof steps are propagated to the initial document and, in particular, “rendered” into the “plain text presentation”.

For CoPs it would be interesting to analyze different proofs wrt. the level of detail.

See MKM Proceedings: Authoring verified documents by interactive proof construction and verification in Text-Editors. (Dominik Dietrich, Ewaryst Schulz, Marc Wagner)

At CICM 2008 (Workshop DML), Stephen Watt presented his work on analyzing the frequency of symbols, that would be an interesting infrastructure for further cop-based analysis.
See Michael’s blog and the DML Proceedings.

Another talk (Workshop MathUI) was on his handwriting recognition of mathematical notations: Presenting his Representation Approach. See paper

The challenge is that there is no fixed dictionary. But maybe CoPs provide some restrictions of potential parsing results? Or is frequency a better approach?

Marc Wagner implemented a plugin for TeXmacs which tracks a user writing and modifying a document. This was done to gain intuitions for extending is Plato editor (identifying the linguistic phenomena). And interesting aspect are that the process of writing of notations is also a practice, not just the selection of a notation. Another aspect is the level of formality users choose to solve their tasks. An analysis of the solutions might be an interesting case study for CoPs.

• Most modification where due to notations errors (so automatic verification would be very helpful).
• Sentences fragments where classified (linguistic ontology to deal with linguistic proofs)
• Pointed out practice for “concluding step”.
• Pointed out practice for “justifying” steps. (partly very hard to parse automatically: specific science or natural language)

Plan for the future: Additional components for the “ideal mathematical assistance system”. Among others

• Linguistic Ontology for concepts, types, theory structures.
• Dynamic Adaptation of Notations (Change Management).
• Context Memory???.

See paper at MathUI 2008