Séminaire – Mathématiques 19e-21e, histoire et philosophie

Michael Harris (Columbia University)
Mechanical understanding of proofs?

Résumé :
The drive to incorporate methods of artificial intelligence in mathematics raises the possibility of the separation of proofs from understanding. A formal proof can be formally validated but not understood by anyone : not by humans, either because the proof is written in impenetrable code or simply because it is too complex ; not by machines, unless the term « understanding » is radically redefined. It may be objected that many existing proofs are too long and intricate for any one person to understand. Nevertheless, it is a common practice to invite the authors to explain such a proof in seminar talks, or for study groups to break down a proof into comprehensible chunks, so that one may speak of a collective (human) understanding. My talk will try to imagine machine-made proofs that cannot be understood even in this way. In the process, I will examine strategies by which mathematicians seek to make proofs understandable ; how one might determine whether or not these strategies have been successful with a human audience ; and what it would mean to test a machine’s understanding of a proof.

The talk will be presented from the standpoint of a practicing mathematician and will take the form of questions of a philosophical nature arising from the practice. If time permits there will also be reports on attempts by large language models to demonstrate understanding of relatively simple proofs.

Clément Bonvoisin (SPHERE, Université Paris Cité)
Computations made proof. On the reassessment of an equation a decade after its writing at RAND Corporation (1948-1961)

Résumé :
In this talk, I wish to discuss the relationship between computations and proofs in contemporary mathematics. I intend to do so by focusing on an equation written by US mathematician Magnus Hestenes (1908–1991). The equation lies in a research memorandum produced by Hestenes in 1950 for the RAND Corporation, a think tank funded by the US Air Forces. The memorandum itself was part of a broader research work on the computation of minimum time flight paths for aircrafts and missiles, which lasted from 1948 through 1951. However, in an article published in 1961, US mathematician Leonard Berkovitz (1924–2009) cited the equation, and framed it as an early version of a result obtained in 1958 by a group of Soviet mathematicians—namely, Pontryagin’s maximum principle.
This situation calls to mind a set of issues for the history of mathematics. How did Berkovitz come to know of this equation, buried in the middle of a report with poor circulation outside of RAND ? What status did the equation play in the initial memorandum, and what role did it play over the 1950’s ? How similar was it to Pontryagin’s maximum principle, and how did it differ from it ? How can we account for the likening of the equation to a result derived some eight years after the memorandum was written ? And what historiographical consequences did such a likening have ? To answer these questions, I will trace the circulations, uses and changes in status of the material contained in Hestenes’ memorandum at RAND over the 1950’s. In doing so, I will show the importance of the initial purpose of the project Hestenes took part in—computations. This, I will argue, shaped the initial status of the equation as a mere intermediate step, rather than as an original result—a status Berkovitz misrepresented in his 1961 article. Overall, I hope to provide insights on the relationship between computations and proofs in mathematics, and on its historiographical consequences.

Lieu : Salle Malevitch (483A) bâtiment Condorcet