“KWARC was!”

Notes on Cristian S. Calude et al. (2007) Proving and Programming (see also previous post, see slides). Please note that the authors do not necessarily share my personal opinions and summaries on this page.

There is a strong analogy between proving theorems in mathematics and writing programs in computer science. Programming gives mathematics a new form of understanding. The computer is the driving force behind these changes.

• “Theorems (in mathematics) correspond to algorithms and not programs (in computer science)”
• “Programs (in computer science) correspond to mathematical models.”
• Proving the correctness of algorithms is seldom a focus in software projects (but: even testing/ documenting is sometimes neglected)
• Do some programming language facilitate/ required to put more focus on the correctness of the algorithms (e.g. functional language such as scala or ML; where programs are closer to mathematical models than in imperative languages)?
• Can bugs be avoided? Can the use of rigorous mathematical proofs guarantee that software and hardware perform as expected?
• Many projects and products dedicated to automated testing of program correctness, for example, VIPER or TestEra (automated testing of Java programs).
• What do proof obligations (Verpflichtung) have to do with the correctness of programs?: e.g. Barthe et al. discuss the “interaction between compilation and verification condition generators (VC generators), which are used in many interactive verification environments to guarantee the correctness of source programs, and by several proof carrying code (PCC) architectures to check the correctness of compiled programs. Such VC generators operate on annotated programs that carry loop invariants and procedure specifications expressed as preconditions and postconditions, and yield a set of proof obligations that must be discharged in order to establish the correctness of the program.” (loop and procedure level; see also specification languages such as CASL for the representation of precondition, invariants, and postconditions, i.e. proofs obligation)
• But correctness proof for a program, adds very little to one’s confidence in the program: “Beware of bugs in the above code: I have only proved it correct, not tried it. (Knuth)” (p.310)
• Checking new types of proofs: probabilistic, experimental, hybrid proofs (computation plus theoretical arguments) (p.311 ff.)

Further readings

• Hayashi (1998): Testing Proofs by Examples

Notes on (1) Cristian S. Calude et al. (2003) Passages of Proof and (2) Cristian S. Calude et al. (2004): Mathematical Proofs at a Crossroad .

Please note that the authors do not necessarily share my personal opinions and summaries on this page.

Stages of mathematics

1. pre-Greek mathematics dominated by observation, intuition, experience
2. Greek deductive mathematics based on theorems; Euclid’s geometry; see also Pythagoras,Thales, Aristotle, Euclid, Archimedis. (Euclid became the reference for axiomatic-deductive thinking, see more recent works in mathematics, physics, computer science, biology, linguistics, which follow this tradition)
3. Mathematical language triggered by need for precision and rigour. Previously ordinary language was used “dominated by imprecision resulting from its predominantly spontaneous use, where emotional factors and lack of care have an impact”. Galilei, Descartes, Newton, Leibniz, … contribute to a shift from ordinary to a mixed language, i.e. ordinary language supplemented by an artificial component of symbols, formulas, and equations
4. The epsilon rigour; 19th century, Cauchy, Weierstrass (coping with processes with infinitely many steps such as limit, continuity, differentiability, and integrability)
5. The challenge of the principle of non–contradiction and the logical crisis (Russell–Whitehead, Hilbert, Brouwer); 19th/20th century; optimistic towards the possibility to arrange the whole mathematics as a formal system and to decide for any possible statement whether it is true or false.
6. Gödel’s incompleteness theorem (1931): “every formal system which is finitely specified, rich enough to include the arithmetic, and consistent (free of contradiction), is incomplete”, distinction between truth and provability (1:p.173 ff.); Chaitin (1975) suggests that complexity is a source of incompleteness
7. Reconciliation of empirical–experimental mathematics with deductive mathematics (today): Four-colour Problem (4CT; 1976; by Kenneth Appel & Wolfgang Haken; proof of 4CT by Neil Robertson, Daniel P. Sanders, Paul Seymour and Robin Thomas ; or the Kepler Conjecture by Thomas Hales) realized by the use of computer programs as pieces of mathematical proof
8. Quantization: Proofs are no longer exclusively based on logic and deduction, but also empirical and experimental.

What is mathematical proof?

• “A proof is a series of logical steps based on some axioms and deduction rules which reaches a desired conclusion. Every step in a proof can be checked for correctness by examining it to ensure that it is logically sound.” (1:p. 171)
• But who checks the proof (as human and Computer agents make mistakes)? Often proofs are falsified after having been published and then corrected (e.g. Appel/ Haken take on Kempe’s ideas). Some proofs cannot be checked by single humans (being to long and/or accomplished by computer-assistance) such as 4CT. (1:p. 171)
• “Mathematics cannot be conceived without proofs: [..] proofs and theorems go together; the object of a proof is to reach a theorem, while theorems are validated by proofs” (1:p.172).
• But: Mathematics is more than proofs. “What the mathematical community seems to value most are ideas. The most respected mathematicians are those with strong intuitions. (Harris)”. (1:p.172)
• Three dimensions of proofs:
  • syntactically: the formal proof, but “proof is only one step in the direction of confidence” (1:p.174, see Edmund Landau)
  • semantically: (truth value) “correctness by itself does not validate a proof, it is also necessary to understand it” (1:p.175; René Thom, Daniel Cohen, William Thurston) “the mission of mathematics is understanding”, consequently, computer-assisted proofs are harder to accept (see 4CT), but also deductive proofs are sometimes only understood by few mathematicians (see 1:p.176), “a theorem is validated if it has been accepted by a general agreement of the mathematical community” (Thom, 1:p.178), “a theorem is a statement that could be checked individually by a mathematician and confirmed also individually by at least two or three mathematicians, each of them working independently” (1:p.178) thus proposing the notion of an “agnogram … a theorem-like statement that we have verified as best we could, but whose truth is not know with the kind of assurance we attach to theorems and about which we must thus remain, to some extend, agnostic” (Swart, 1:p.178), “we believe the experts and we cannot tell for ourselves” (1:p.179), “mathematics occupies a special place [among other disciplines], where we believe anyone who claims to have proved a theorem on the say – so of just a few people – that is, until we hear otherwise” (1:p.179), “… in mathematics you can really argue that this is as close to absolute truth as you can get (Joe Spencer)” (1:p.179)
  • pragmatical: (relevance & use) “truth is not where you find it, but where you put it” (Perlis). “no matter how precise the rules are, we need human consciousness to apply the rules and to understand them and their consequences” (1:p.183)
• Aspects of mathematical proofs: deduction/ syllogistic reasoning (most visible aspect), but also: observation, intuition, experiment, visual representations, induction, analogy, and examples; some belonging to the preliminary steps, whose presence is not made explicit (when finally presenting the proof), but without which proofs cannot be conceived (2-p.17; see previous post); proving is a very heterogeneous process

In real life proofs may be different …

• Proof by obviousness: “The proof is so clear that it need not be mentioned.”
• Proof by general agreement: “All in favour?”
• Proof by calculus: “This proof requires calculus, so we’ll skip it.”
• Proof by lost reference: “I know I saw it somewhere”
• Proof by necessity: “It had better be true, or the entire structure of mathematics would crumble to the ground.”
• Proof by plausibility: “It sounds good, so it must be true.”
• Proof by intimidation: “Don’t be stupid; of course it’s true.”
• Proof by terror: When intimidation fails
• Proof by lack of sufficient time: “Because of the time constraint, I’ll leave the proof to you.”
• Proof by tessellation: “This proof is the same as the last.”
• Proof by majority rule: Only to be used if general agreement is impossible
• Proof by authority: “Well, Don’t Knuth says it’s true, so it must be!”
• Proof by intuition: “I just have this gut feeling”

Towards Artificial Mathematics and quasi-empirical proofs

• equivalence between the logical and computational proofs
• logical/ conventional proofs: traditional; reasoning of humans (see Euclid, …); the logical process, i.e. finding a finite sequence of sentences strictly obeying some axioms and inference rules
• computational/ unconventional: computational process (machines are constructed based on sequences of sentences by humans) producing these sequences; but: proofs can contain steps that can never be verified by humans (based on the equivalence: development of artificial mathematicians, i.e. theorem provers such as Mathematica, Maple, MathLab)
• classical but unconventional proofs also comprise classical proof of excessive length and complexity (e.g. the classification of finite simple groups; 1:p.176/183)
• Artificial mathematicians are far less ingenious and subtle than human mathematicians, but they surpass their human counterparts by being infinitely more patient and diligent.
• Towards quantum computational proofs: conversion from computation into a sequence of sentences may not longer be possible, quantum automation are able to check a proof, but fail to reveal a “trace” of the proof (we don’t why it true), (quasi-empirical) quantum proofs might influence how we learn/ understand mathematics; leading to new ways to understand (and practice) mathematics, although we might not fully accept/trust unconventional proofs, the computational result is “a mathematical activity because it advances our knowledge of mathematics” (1:p.184)
• Overall: “There is little difference between traditional and unconventional types of proofs as [..] i) mathematical truth cannot always be certified by proof, ii) correctness is not absolute, but almost certain, as mathematics advance by making mistakes and correcting and re-correcting them (see Lakatos), iii) non-deterministic and probabilistic proofs do not allow mistakes in the applications of rules, the are just indirect forms of checking, iv) the explanatory component, the understanding emerging from proofs [..] is subjective and has no bearing on formal correctness.” (1:p.184)
• “Experimental Mathematics – as systematic mathematical experimentation ranging from hypotheses building to assisted proofs and automated proof-checking-will play an increasingly important role and will become part of the mainstream of mathematics. There are many reasons for this trend: They range from logical (the absolute truth simply doesn’t exist), sociological (correctness is not absolute [..]), economic (powerful computers will be accessible to more and more people), and psychological (results and success inspire emulation)” (2-p.26)

Knowledge is acquired through reason and by experiment: Should proofs belong exclusively to logic? Or should we also accept empirical-experimental arguments? Towards blending logical and empirical-experimental arguments. There is hope for integration! (see also next post)

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.”