Workshop on The Notion of Proof
We have already witnessed the moment where chess-playing computers have surpassed humans. It might seem to be only a matter of time that computers will also surpass humans in mathematical theorem proving. In fact, the traditional notion of mathematical proof faces in the 21st century what we will call “the computer challenge”. Three different aspects are worth separating:
- proof search;
- proof check;
- proof representation.
Proof search has its known limitations due to undecidability and complexity results. However, special areas, such as semigroup theory, already enjoy considerable support from computer-generated proofs. Proof check is recently the “hottest” area, in no small part due to the attempt to formally verify the proof of the Kepler Conjecture by its author Hales. Proof representation seems currently to be a stumbling block for convincing the mathematical community to accept computer-aided theorem proving as a viable complement to everyday mathematical research.
For our workshop we solicit contributions for discussions about the current state-of-the-art of automated theorem proving (ATP), approaching the topic from the mathematical (or even philosophical) side, as well as from computer science. In addition to standard scientific/philosophical papers, descriptions and demonstrations of computer systems that bear on these issues are also welcome. Special focus is put on the last two items mentioned above, addressing the more concrete questions:
- How, and to what extent, can (or will) proof checking convince the mathematical community from the correctness of a proof?
- Does computer generated proof representations match with our intuitive notion of mathematical proof?
The answers to both question should give us a deeper insight in the challenges and tasks for mathematical proofs and computer-aided theorem proving in the 21st century.
Organisers
Invited speakers
Important dates
- May 31
- Submission deadline
- June 10
- Author notification
- July 7–11
- CICM 2014
- July 8
- Workshop
Call for Papers
Contributors can submit a 1–2 page abstract via Easychair. Submissions will be selected for presentation by the organizers with the possible assistance of external reviewers, as warranted.
If the quality of the contributions warrants it, we intend to invite
contributors to expand their abstracts/talks into more complete papers.
Program
Mark Adams (FireEye, Germany), “Proof Auditing for Formalised Mathematics”
Groundbreaking mathematics formalisation has been achieved in recent years with the reproduction of three significant mathematical results inside theorem provers: The Four Colour Theorem and the Feit-Thompson Lemma inside Coq, and the Kepler Conjecture inside HOL Light. These efforts have significantly increased the confidence in these results, each of which have substantial original proofs that run to a few hundred pages of mathematical text and, in the case of the Four Colour Theorem and the Kepler Conjecture, at least a few thousand lines of computer source code.
However, it is a valid question to ask whether these formalisations have indeed established their claimed results, rather than to simply trust that the result has been proved. An inquisitive user can download the proof scripts for a given project, replay them through the theorem prover, and observe the output. However watching hundreds of screenloads of output whizz past is unlikely to be enlightening unless the user knows exactly what to look out for.
We propose a rigorous process of independent assessment by an expert, that is as objective as possible and suitably sceptical, not assuming anything about the reputation of the people carrying out the formalisation, and taking into account the weaknesses of the theorem prover being used. We call this process a "proof audit". Perhaps surprisingly to those outside the field of theorem proving, proof auditing is not generally carried out on large proof formalisations. William Farmer (McMaster University, Canada), “Can Computer Proving Replace Traditional Proving?”
Mathematics is the process of creating, exploring, and interrelating mathematical models. Proving is the act of deriving logical consequences. It is the most powerful and most important tool for doing mathematics, particularly for exploring mathematical models. Proving is traditionally done with the aid of little more than pencil and paper. Performed with computers, computer proving has advantages over traditional proving that are very compelling. But can computer proving replace traditional proving? Our thesis is that computer proving in its current form cannot entirely replace traditional proving, but computer proving will in time, with suitable advances in mechanized mathematics, replace traditional proving just as text editing on a computer has replaced typing on a typewriter. Jamie Gaspar (Rovira i Virgili University, Spain and New University of Lisbon, Portugal), “Short introduction by example to Coq”
Proof assistants are computer programs that help mathematicians to prove theorems and to formally verify the correctness of proofs. Proof assistants are nowadays one of the more exciting areas in the intersection of mathematical logic and computer science. For example, one particularly exciting achievement is the formal verification of the proof of the four colour theorem using the proof assistant Coq.
In this talk we give a very elementary introduction to Coq by means of a very simple example: the proofs of the theorems
- if ≤ is a non-strict partial order, then < defined by x < y ↔ x ≤ y ∧ x ≠ y is a strict partial order;
- if < is a strict partial order, then ≤ defined by x ≤ y ↔ x < y ∨ x = y is a non-strict partial order.
Then we end by discussing what is achieved with this kind of formal verification. We keep this talk short, simple and sweet. Arie Hinkis (Cohn Institute for the History and Philosophy of Science and Ideas, Tel Aviv University, Israel), “The representation of mathematical proof through gestalt and metaphors”
Conjecture: Every mathematical proof can be presented as a sequence of gestalt switches, each obtained by a metaphor.
A gestalt of a mathematical proof is the way the arrangement of its details is perceived. A gestalt switch occurs when a gestalt is replaced by another. A metaphor is a description of the way a gestalt switch is obtained. Metaphors and gestalts of a proof may contain both mathematical and non-mathematical notions. The gestalts and metaphors of a proof I call 'proof descriptors'. The search for the proof descriptors of a proof I call 'proof-processing'. Proof descriptors provide a way to compare proofs. The comparison of different proofs given to the same theorem may enrich its meaning. Shared proof descriptors in proofs to different theorems may suggest how the later proofs were won from previous proofs. Thus the notion of the internal history of mathematics emerges. Proofs influence the development of mathematics at least as much as theorems. Through proof descriptors proofs may obtain popular presentation. Proof descriptors may provide new links with non-mathematical works of art and poetry. There is room for idiosyncrasy in the generation of metaphors for proofs. The latter are especially of interest as they are rarely pointed out in mathematical texts, but are apparently used in informal discourse among peers. Gestalt signifies static elements of a proof, which are in general rather easy to identify, while metaphor signifies dynamic elements, i.e., constructions. Proof descriptors may relate only to parts of a proof. In fact, it is by its proof descriptors that a part is discerned. Descriptors may serve as mnemonics of repeated patterns. Descriptors are not necessarily verbal; they may include drawings or gestures. The informal character of proof descriptors is of their essence.
Conjecture: Mathematicians always proof-process the proofs that they learn. Proof descriptors thus form the arsenal from which mathematicians draw their means for new proofs.
The lecture will provide examples of proof descriptors, especially from the context of the Cantor-Bernstein Theorem and Bernstein Division Theorem. Michael Kinyon (University of Denver, United States): “Quasigroups, Loops and Automated Deduction, or How I Learned To Stop Worrying and Start Letting Computers Prove Theorems”
Since the turn of the millennium, there has been a slow but steady increase in the use of automated deduction software in different areas of algebra, such as lattice theory and semigroup theory. In this talk I will discuss how my collaborators and I have used automated deduction tools such as OTTER, Prover9 and Waldmeister to crack hitherto unsolved problems in quasigroup/loop theory. In the last couple of years, the problems we are attempting to attack are pushing the available software to its limits. I will close by discussing some of the implications of this for human understanding of proofs generated by software.
No background in quasigroup/loop theory is needed or expected.
Ursula Martin (University of Oxford, United Kingdom), “Is mathematics a social machine?”
The social is crucial in the production of mathematics, and in recent years a research field of mathematical practice has emerged, drawing together sociologists, philosophers, educationalists, cognitive scientists and mathematicians themselves to understand the production of mathematics, knowledge that in turn can feed into designing better social machines for mathematics. Collaborative systems such as polymath contribute to mathematics research, and also provide a rich evidence base for further understanding of mathematical practice. The emergence of forums and blogs will, if used as a serious research tool by mathematicians, provide many more clues as to the way in which they think, since they display and record thought processes in informal mathematics in a completely unprecedented way. This can be used to characterize patterns of reasoning which emerge via social interaction and collaborative mathematics.
For example, our analysis of a polymath proof found only 47% of the conversational ‘turns’ were proof steps, with the rest being made up of conjectures, discussions of examples, and social moves, which, although they did not contribute technical content, were essential to keeping the discussion going. Confirmation was also found of Lakatos’s notions of how mathematics advances, for example his analysis of the role of counterexamples and error.
‘Social machines’ are a new paradigm, identified by Berners-Lee in his 1999 book ‘Weaving the Web’ [3], for viewing a combination of people and computers as a single problem-solving entity. Berners-Lee describes a dream of collaborating through shared knowledge:
Real life is and must be full of all kinds of social constraint—the very processes from which society arises. Computers can help if we use them to create abstract social machines on the Web: processes in which the people do the creative work and the machine does the administration... The stage is set for an evolutionary growth of new social engines. The ability to create new forms of social process would be given to the world at large, and development would be rapid.
For science, social machines provide platforms for sharing knowledge, leading to innovation, discovery, and commercial opportunity, a perspective set out in Michael Nielsen’s 2011 book ‘A new kind of science’. For example, Galaxy Zoo allows members of the public to look for features of interest in images of galaxies, and Foldit is an online game where users solve protein folding problems. Future more ambitious social machines will combine social involvement and sophisticated automation, and are now the subject of major research, for example in Southampton’s SOCIAM project following an agenda laid out by Hendler and Berners-Lee [35]. This approach builds on e-Science work such as Goble’s myExperiment, a collaborative research space for scientific workflow management and experiment, widely used in bioinformatics to document and share data, annotations, experiments and results. Bicarregui and colleagues provided a convincing picture of how the semantic web and the infrastructure of e-science provided the elements needed, should we wish to make collaborative verification a reality.
Researchers are already bringing the social to computational logic: for example Tom Hales crowdsourced, with a team of mathematicians in Vietnam, parts of the formal proof of the Kepler conjecture; a team led by Voevedsky collaborated intensively during a semester in Princeton to instigate the new field of homotopy type theory, underpinned by a body of formal proof in Agda; and Jacques Fleuriot and his colleagues in Edinburgh have recently launched the ProofPeer system for collaborative proving. Freek Wiedijk (Radboud University Nijmegen, the Netherlands): Extreme mathematics
The computer is changing how mathematics is being done. I'll sketch an extreme system for doing mathematics by computer.
|
