- 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.
Discussion with Cristian Calude
3 Responses to “Discussion with Cristian Calude”
Leave a Reply
You must be logged in to post a comment.