Preuve Proof Prueba

Web Newsletter
Mars/Avril 1997

La bibliographie
The bibliography
La bibliografia

Au lecteur ...
La partie principale de cette bibliographie est constituée d'articles publiés dans des revues, des livres et des chapitres de livres accessibles par les réseaux de distribution ordinaires, ainsi qu'aux thèses. Je compte sur les remarques et suggestions des utilisateurs pour améliorer cet outil.

Al lector ...
La parte principal de esta bibliografía es constituida por artículos publicados en revistas, libros y capítulos de libros accesibles por las redes de distribución ordinarias, igualmente las tesis. Yo cuento con las remarcas y sugestiones de los utilizadores para el mejoramiento de este útil.

To the Reader ...
This bibliography consists to a large part of articles published in journals, of books, and of chapters of books, all accessible from normal sources, as well as of theses. I am counting on remarks and suggestions from users to improve this tool.

Nicolas Balacheff


Dreyfus T., Hadas N. (1996) Proof as answer to the question why. Zentralblatt für Didaktik der Mathematik 28 (1) 1-5.

Hanna G., Jahnke N. (1996) Proof and Proving. In: Bishop A. et al (eds.) (pp.877-908). International Handbook of Mathematics Education. Dordrecht: Kluwer Academic Publishers.

Paolo Boero "on-line", les textes sur la Preuve présentés à PME par Paolo Boero et de ses collègues :

(1994) Approaching rational geometry: from physical relationships to conditional statements.
(1995) Towards Statements and Proofs in Elementary Arithmetic: An Exploratory Study about the Role of Teachers and the Behaviour of Students.
(1996) Some dynamic mental processes underlying producing and proving conjectures.
(1996) Challenging the traditional school approach to theorems: a hypothesis about the cognitive unity of theorems.


A talk on proof

Midlands Mathematics Education Seminars
University of Warwick
Institute of Education

"Students teachers' encounters with formal proof: convincing themselves and convincing others"

By: Janet Ainley, Marcia Pinto and David Tall

In this seminar we shall contrast the experiences of students taking a course in Mathematical Analysis within an education degree with those of undergraduates following a traditional mathematics programme. We shall explore the idea that to train student teachers to be "good mathematicians" by introducing them to formal axiomatic methods may be counterproductive because there is a conflict between their professional intention as teachers and the formalism of mathematical proof.

Proofs and mathematical structure

A discussion from the NCTM-L archive
hosted by the Math Forum

Do the NCTM Standards give short shrift to what is arguably the most basic and vital mathematical structure of all: proof? If so, does this constitute rejecting mathematical structure?

In a previous discussion, "Parent's messages," a contributor suggested that readers search the Standards for occurrences of the word 'proof'. This conversation, "Proofs and Mathematical Structure," takes up the effect of the word's omission, the need for and value of precise mathematical arguments, the difficulty of translating everyday language into a form that can be analyzed, and the call for manuscripts addressing the role and nature of proof in a Standards-based curriculum.

The NCTM Standards are available on the Web at

Un exposé sur la preuve
9 mars 1997
Séminaire National de
Didactique des Mathématiques

"Les mathématiques discrètes : une alternative à la géometrie pour L'apprentissage de la preuve ? Débat à partir de quelques méthodes spécifiques (induction, cage à pigeons, coloration).

Par: Denise Grenier, Charles Payan
Laboratoire Leibniz, CNRS, INPG et UJF Grenoble

Philippe Bernat

Enseignant chercheur au CRIN de Nancy, Philippe Bernat fut l'un des artisans du développement de nouveaux environnements pour l'enseignement de la géométrie. Ses travaux de recherche actuels, à la suite sa thèse, portaient sur la conception et le développement de CHYPRE, un environnement d'aide à la résolution de problèmes de géométrie et de construction de preuve pour des élèves de collège. Ces travaux ont été brutalement interrompus par le décés de Philippe Bernat fin décembre 1996. Attentif et enthousiaste, il fut le premier à contribuer à ce site sur la Preuve. Nous saluons sa mémoire.


The presentation of formal proofs

an AI PhD thesis by Martin Simon
Technische Universität Berlin, 1996

In this thesis is presented an approach to the intelligible communication of formal proofs. Observing a close correspondence between the activities of formal-proof development and program development, and using this as a guideline, the author applies well-known principles from program design to proof design and presentation, resulting in formal proofs presented in a literate style, that are hierarchically structured, and that emphasize calculation.

more :

From the Mathedu Archive:
Proof by induction

Prof. Williams P. Wardlaw writes: "I like to introduce induction with a story about painting a chain. Given my institution, I prefer an anchor chain. A First Lieutenant (responsible for painting) orders a Seaman to paint the anchor chain. Later he asks the Seaman what color he painted the chain. The Seaman cannot remember, but is sure that whatever color he painted a given link, he used the same color for the next link. The First Lieutenant goes on deck and sees that the first link, just showing at the top of the hawse pipe, is chartreuse. What color is (every link of) the chain?"
  The story is followed by a formal discussion of induction and several examples, such as a couple of summation formulas and a couple of inequalities...
  Lou Talman adds: Sonneborn's Horse Lemma states that all horses are the same color. Its power lies in its immediate applicability to proofs by contradiction, which assume the form "Suppose it were not so. Well, that would be a horse of another color, wouldn't it."

This searchable thread from the MATHEDU archive cites useful articles and discusses examples of mathematical proof by induction at both the high school and the college level.

Ce pourrait être un proverbe...

"L'arithmétique le montre, l'expérience le prouve"

un homme politique des années 70, sur France Inter.

News from the Budapest Seminar
January 1997

Arzarello F. (1997) For an ecology of proof in the classroom.

An AI Call for Paper and Participation

First International Workshop on Proof Transformation and Presentation

April 8-10, 1997
Castle Dagstuhl, Octavieallee, 66687 Wadern, Saarland, Germany

Over the past thirty years there has been significant progress in the field of automated theorem proving with respect to the reasoning power of the inference engines: many hard and open mathematical problems could be proven with a machine and the use of formal methods in software engineering and hardware verification is becoming a reality.

Another important ingredients of a automated reasoning system, however, is its ability to communicate with its users. For many applications such as in a mathematical reasoning assistant, an effective communication between the system and its users is critical for the acceptance of a system. Only if a system also talks his language, a user will be convinced by machine-found proofs and feel his understanding of the topic improved.

Many standard representations used by ATP systems such as resolution proofs or mating proofs, unfortunately, are difficult to follow even for professional mathematicians. This holds even more so, as the machine generated proofs become more complex (between several hundred and up to several thousand steps in a single proof). Therefore there has been a increasing interest in the transformation and presentation of machine-found proofs. Techniques have been developed to transform proofs from a machine-oriented formalism into a more readable formalism such as natural deduction (ND) and to abstract and restructure these machine-generated proofs to produce a textbook style of proofs in natural language. Another related line of research concerns the interactive, graphic or multimedia interface facilities for theorem provers.

This informal workshop aims to create an intimate and stimulating setting to bring together researcher from various fields working with or interested in this exciting issue to exchange ideas and results.

Electronic submissions of one page are solicited. Proceedings containing an extended version will be published afterwards in a suitable form. Other people interested in participating are invited to submit a short description of background and research interest. To encourage a workshop atmosphere, priority will be given to those who submitted a paper.

Topics include (but are not restricted to)

1. Relationship between logic calculi, including complexity measures,
2. Mathematical vernacular
3. Transformation of proofs from a machine-oriented formalism to a more readable formalism like natural deduction
4. Abstraction and Restructuring of machine-found proofs
5. Analysis of user requirements for the interface of ATP systems
6. Cognitive models of human deduction
7. Verbalization of machine-found (formal) proofs in natural language
Submission deadline
Feb. 28, 1997

Submission and Contact:

Further information:

Program Committee

Xiaorong Huang  Univ. of Toronto/DFKI
Jaff Pelletier  Univ. of Alberta
Frank Pfenning  Carnegie Mellon Univ.
Joerg Siekmann  German Research Centre for Artificial Intelligence (DFKI)
Other call for papers

Dead line 15 june 1997.
"The rôle of proof through out the curriculum" (fall 1998 issue)
Mathematics Teachers, NCTM, 1906 Association Drive Reston, VA 22091-1593, USA

NCTM 1999 Yearbook on Mathematical reasoning.
Information and guidelines:  under "Educational Materials / 1999 Yearbook"

See also Proof Newsletter January/February 1997

Lettres précédentes
Past Newsletters
Noticias anteriores

97 01/02