Showing 1–2 of 2 results for author: Lamport, L

Mathematical Proof Between Generations

Authors: Jonas Bayer, Christoph Benzmüller, Kevin Buzzard, Marco David, Leslie Lamport, Yuri Matiyasevich, Lawrence Paulson, Dierk Schleicher, Benedikt Stock, Efim Zelmanov

Abstract: A proof is one of the most important concepts of mathematics. However, there is a striking difference between how a proof is defined in theory and how it is used in practice. This puts the unique status of mathematics as exact science into peril. Now may be the time to reconcile theory and practice, i.e. precision and intuition, through the advent of computer proof assistants. For the most time th… ▽ More A proof is one of the most important concepts of mathematics. However, there is a striking difference between how a proof is defined in theory and how it is used in practice. This puts the unique status of mathematics as exact science into peril. Now may be the time to reconcile theory and practice, i.e. precision and intuition, through the advent of computer proof assistants. For the most time this has been a topic for experts in specialized communities. However, mathematical proofs have become increasingly sophisticated, stretching the boundaries of what is humanly comprehensible, so that leading mathematicians have asked for formal verification of their proofs. At the same time, major theorems in mathematics have recently been computer-verified by people from outside of these communities, even by beginning students. This article investigates the gap between the different definitions of a proof and possibilities to build bridges. It is written as a polemic or a collage by different members of the communities in mathematics and computer science at different stages of their careers, challenging well-known preconceptions and exploring new perspectives. △ Less

Submitted 8 July, 2022; originally announced July 2022.

Comments: 17 pages, 1 figure

Journal ref: Notices of the American Mathematical Society (January 2024), Vol. 71, No. 1, pp. 79-92

On the Glitch Phenomenon

Authors: Leslie Lamport, Richard Palais

Abstract: The Principle of the Glitch states that for any device which makes a discrete decision based upon a continuous range of possible inputs, there are inputs for which it will take arbitrarily long to reach a decision. The appropriate mathematical setting for studying this principle is described. This involves defining the concept of continuity for mappings on sets of functions. It can then be shown t… ▽ More The Principle of the Glitch states that for any device which makes a discrete decision based upon a continuous range of possible inputs, there are inputs for which it will take arbitrarily long to reach a decision. The appropriate mathematical setting for studying this principle is described. This involves defining the concept of continuity for mappings on sets of functions. It can then be shown that the glitch principle follows from the continuous behavior of the device. △ Less

Submitted 4 April, 2017; originally announced April 2017.

Comments: In November 1976, this paper was rejected by the IEEE Transactions on Computers because the engineers who reviewed it could not understand the mathematics. Six years later, the journal apparently acquired more mathematically sophisticated reviewers, and it published a less general result with a more complicated proof