My second meeting with Cristian Calude has clarified some of the issues from the first meeting …
Please note that Cris does not necessarily share my personal opinions and summaries on this page.
- Confidence in and Acceptance of proofs: In the previous meeting, I haven’t be sure about what Cris means with context. Cris means by this, that the confidence in a theorem increases by the number of applications, i.e. the number of times it is reused by others e.g. to prove another theorem. This application can be interpreted in two ways: (1) Other mathematicians understood the prove and (2) the mathematical community assessed this contribution to be relevant. In particular, Cris again pointed out that there a several dimensions of a accepted and significant theorem: Neither beauty nor correctness are enough, but it also has to be understood and used by the community, i.e. it needs to be relevant and useful for further mathematical work.
- Reusing trusted and correct Theorems: Cris illustrated today how critical it is to reuse only trusted and correct theorems and that even then mathematicians have no certainty as there is no absolute correctness: In 1988, Yoichi Miyaoka, number theorist at the Max Planck Institute in Bonn, claimed that he had proven the Fermat’s Theorem (eventually proved by A. Wiles). As I was told, his actual proof was not the direct flaw, but when checking his proof step-by-step, the professional referees identified that one of the theorems he re-used was incorrect. However, that theorem had been published and reused by other mathematicians, but had not been carefully checked so far (cf. NY Time). This is a phenomena I have heard before, i.e. sometimes proofs without central interest to the community are not extensively checked.
- Mathematics and Computers: As far as I understood, Cris is interested in integrating traditional and unconventional mathematics, i.e. axiomatic-deductive thinking and computer-supported experimenting to finally achieve a proof. He believes that mathematical proofs will more and more be checked by computers. Of course, this will be a gradual process, from solely human referees to fully automatized proof checking. In our last meeting, we identified to ways of addressing the problem of bringing mathematicians and computers closer together: (1) less formal and human-friendly systems and (2) new ways (of thinking and the respective tools) for encoding mathematical knowledge. Cris is envisioning a process that will support authors to convert their proofs (consisting of text and formulae) to fully formal formats that can be object of automatic provers. In a first step, he would like to see that we can distinguish pure comments from text that is part of the proof. This would require tools and a respective representation format for mathematical documents: The tools need to (semi-)automatize the annotation of mathematical text. Different technologies can be of use from natural language parsing to semi-automated semantic annotation ideally integrated in the publication processes of mathematicians (see sTeX as semantic extension for LaTeX; invasive editors for MS PPT and Word; Sentido; and SWiM). The format has to support the mark-up of narrative, rhetorical, but also mathematical concepts (see OMDoc and its extension in the 2.0 version). However, apart from the format and tools, Cris vision also includes a social aspect that has to evolve over time, i.e. mathematicians have to trust in computer-checked proofs and they actually have to use the tools for formalizing their documents and this leads us to an ongoing-discussion, also referred to as authoring-dilemma (see Andrea’s work).
- Collaboration with Cris: Potentially, Cris and I will work on a programmatic paper of what one should do to help integrating traditional and new mathematical practice, i.e. to motivate our this vision and to give concrete suggestion on how to realize it step by step. However, in a next meeting I will introduce him to my work and areas I am involved in, from there on we will make further decision. I will also give a seminar talk here in some weeks to introduce my work to the CS/ math department.
[...] were used by Immanuel and Florian to do their PhD on logic translation and theory management; see next meeting). To sum up, a proof is not necessarily correct, but its confidence can [...]
Discussion with Normen:
It will be quite challenging to address approach (2) above as some mathematical proofs include a number of gaps and, thus, are really hard to formalized. Some mathematicians are neither willing nor do they seem to have the ability (yet) to encode their knowledge in a way that it can be easily converted into machine-readable formats.
If we require professional mathematicians to fill all gaps, we will hamper digitalization of mathematics. Ideally, tools for professional mathematicians would allow them to include gaps and talk on very abstract level. But where is the border of granularity these tools would need? How many gaps can you allow and what background knowledge needs to be provided?
If we allow professional mathematicians to digitalized proofs with gaps, this mathematical knowledge will not be accessible to all users, thus contradicting with the vision of mathematical knowledge management, which aims at making mathematics accessible to all. Instead, we would require users to have some basic mathematical understanding. This sounds reasonable on a first glimpse, but where do we draw the line? Do we expect that all users have elementary school,secondary/ high school or university education?
Without respective tools (e.g. formulae editor), scientists are not encourage to digitalize their mathematical thoughts directly. However, some tools provide intuitive interfaces and languages (in particular for logicians, maybe not for all mathematicians in general): Functional languages (such as ML, HASKELL, Scala) provide very intuitive ways of writing mathematics (currying, uncurrying): They are very close to the formal mathematical language and provide type inferences and therefore type soundness. These languages illustrate that it is possible to design a syntax that allows to model mathematical structures; basically allowing to write mathematics with very little system-dependent adaptations (Normen illustrated several examples).
Regarding the trust in computers, some users of system such as Mathematica and Maple seem have full trust (“blindes Vertrauen”) in the systems and their type inferences.
Normen pointed to Plato, developed by Marc Wagner, Omega Group, University of Saarbrücken, Germany. Plato provides an intuitive interface (LaTeX-based syntax for mathematical notations, mark-up of other document fragments such as definitions, proofs) and is integrated with the Omega system, which it used to automatically evaluate/ verify the mathematical parts of the documents.
Normen also mentioned work that we have seen at the MKM: An approach that allows to digitalize mathematics on a very abstract level and that uses heuristics and tactics to break down these abstract statements into a machine-readable form.
[...] have the feeling that the challenge of bringing mathematicians and computers closer together, requires a lot of expertise in the field of pure mathematics and the more [...]