“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).

Aaron Sloman: Talk is online. His work also emphasize the need of not enforcing representation and practice but taking existing evolutions and, in particular, philosophy into account. So is this a motivation for me to look at mathematical philosophy for understanding mathematical practice?

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.

See MathUI paper. Annotea-Extension for Proof Documents.

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)