“KWARC was!”

My first meeting with Cristian Calude has brought up many interesting aspects and thoughts, I shortly sketch here and I do not yet fully understand …
Please note that Cris and all other researchers mention do not necessarily share my personal opinions and summaries on this page.

• Mathematical Collaboration: In mathematics (and other disciplines), interdisciplinary authors often only know parts of the paper they co-author. If you contact one for the authors, your are sometimes directed to the original writer, as your contact might now able to tell you about all paragraphs in the paper. Cris has experienced this during papers with Chaitin, also both are well-experienced mathematicians, they have different ways of thinking (more visual in contrast to more analytical thinking), which sometimes made it difficult to understand each other’s solution.
• Mathematical Proofs: Cris’s friend, a logician, never looks at proofs. If he likes a theorem, he tries to proof it himself, but studying other people’s proof is not of interest for him
• Mathematical Practice: There is a research group of ethno-mathematicians here at the University of Auckland (e.g. see Bill Barton) looking at questions such as: How does the mother tongue language influence mathematics? Are the metaphors in different languages the same?
• Struggling with Notations: When giving a lecture in Leibzig, Chris experienced that the students struggled with his lecture. They understood the ideas, but when it came to solving assignments and applying the concepts in the lecture, they struggled with notations introduced by Chris as they had learned others.
• Mathematicians and Computers: Chris pointed to an interesting question: How can we train mathematicians to use computers and not to be afraid of their results (i.e. trust in automatic proofs)?. Many parts are implicit when proving, but computers need everything explicated. We have to ways of bringing mathematicians and computers closer together: (1) Making automatic provers more accessible and human-oriented, i.e. decreasing the level of formality needed for interacting with formal prove systems (see MKM proceedings on e.g. Mizar, i.e. “an attempt to reconstruct mathematical vernacular into a formal language which can be read by humans and also verified by software”, or Coq, Mathematica) and (2) Training mathematicians so that their encodings are more accessible for machines, i.e. in order to use computers, mathematicians need to change their way of encoding knowledge.
• Mathematicians and Computers: For (2), Chris suggested to start at looking at referee processes: What kind of questions does a referee ask? What aspects do mathematical referee look at? They mostly do not fully check the presented proof and pose specific questions which may help us to identify how knowledge has to be encoded to be communicated more efficiently (between humans and eventually between humans and computers).
• Mathematical Practice: There are two processes in mathematics: (1) The process of discovery, which is very informal, includes several gaps, and is a slow and iterative approaching of a more and more coherent solution. (2) The process of presenting a result, i.e. the writing up of a solution. Both processes are valuable. We know several tools supporting (2) and in our group we also aim at supporting this process (with a Wiki for collaborative editing and a management of change system, …). However, process (1) requires tools that do not kill the creativity of mathematicians, i.e. that do not enforce notations/ styles and require tedious and correct mark-up of thoughts … but leave room for intuitions, gaps, and mistakes. And also eLearning systems (e.g. panta-rhei) should support process (1) as mathematical education should not focus on the presentation of results but should teach students how to discover math. However, towards the end of process (1), mathematicians might have to/ want to draw on computers (theorem provers and computer algebra systems) to verify their results.
• Confidence in and Acceptance of proofs: In mathematics we observe different degrees of confidence of a proof, i.e. a proof is accepted in a social process and on different layers: (1) It can be published in a journal (and thus reviewed and accepted by the journal chairs) and (2) it can be accepted by reviewers of the two reviewing databases, Mathematical Reviews and Zentralblatt, and (3) it can be certified (i.e. verified by computers; see e.g. Coquand et al). Moreover, (4) the credibility of a theory increases with the number of proofs for its theorems (see e.g. collection of 79 approaches to proving the Pythagorean theorem) and its use in different context (I am not yet sure what Cris means by context. My first guess is that this relates to the reuse of a theory and its interrelation to other theories, i.e. the number of views and theory morphism. Basically, the structures that 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 increase.
• Communal Acceptance: The Clay Mathematics Institute of Cambridge, Massachusetts (CMI) nominates its Millennium Prize Problems for one million dollar. The respective proof has to be published and resist community testing for 2 years. Thus, the mathematical community is very aware of the fact that only publishing a proof does not mean that it is correct.

Further readings

• Cristian S. Calude etAl (2003): Passages of Proof (see my notes; slides)
• Cristian S. Calude etAl (2004): Mathematical Proofs at a Crossroad? (see my notes)
• Cristian S. Calude etAl (2007): Proving and Programming (slides)
• Calude/ Chaitin (2006) A Dialogue on Mathematics & Physics
• see Platonic universe of mathematical ideas
• Ethnomathematics and its First International Congress (the why’s and when of etchnomathematics)
• Bill Barton (1996): Ethnomathematics: Exploring Cultural Diversity in Mathematics (also recommended by Patrick Johnson)
• 2000 Mathematics Subject Classification (pdf)
• “Formalizing mathematical proofs has as aim to represent arbitrary mathematical notions and proofs on a computer in order to construct a database of certified results useful to learn and develop the subject [..]” such as the proof-assistant Mizar, Coq, etc. (cf. Barendregt)
• Coquand et al (2003): [..] a certificate … represents the information needed to complete a proof of correctness of the mathematical data.
• newscientist.com (2006) Mathematical proofs getting harder to verify: “A mathematical proof is irrefutably true, a manifestation of pure logic. But an increasing number of mathematical proofs are now impossible to verify with absolute certainty, according to experts in the field.”