Proof assistants: History, ideas and future
The work
| Authors | Herman Geuvers |
|---|---|
| Editors | |
| Type | article |
| Year | 2009 |
| Citekey | geuvers2009proof |
Where it appeared
| Published in | Sādhanā |
|---|---|
| Volume | 34 |
| Issue | 1 |
| Pages | 3--25 |
Abstract
In this paper I will discuss the fundamental ideas behind proof assistants: What are they and what is a proof anyway? I give a short history of the main ideas, emphasizing the way they ensure the correctness of the mathematics formalized. I will also briefly discuss the places where proof assistants are used and how we envision their extended use in the future. While being an introduction into the world of proof assistants and the main issues behind them, this paper is also a position paper that pushes the further use of proof assistants. We believe that these systems will become the future of mathematics, where definitions, statements, computations and proofs are all available in a computerized form. An important application is and will be in computer supported modelling and verification of systems. But there is still a long road ahead and I will indicate what we believe is needed for the further proliferation of proof assistants.
A copy is held
pdf, 347.5 kB. Not published — it may be under copyright. The facts and links here are.
How it got here
| How it got here | agent via bibtex |
|---|---|
| Added | 2026-08-05 00:00 UTC |
| Approved by | a person 2026-08-14 11:33 UTC |
Filed under
Cite it as
@article{geuvers2009proof,
title = {Proof assistants: History, ideas and future},
author = {Herman Geuvers},
year = {2009},
journal = {Sādhanā},
volume = {34},
number = {1},
pages = {3--25},
}
This record lives at https://refs.drheap.org/geuvers2009proof/ and will keep doing so.