Project : logical
Section: Scientific Foundations
Keywords : proof assistant, correctness, tactic language.
Proof assistants
The first operation that a proof assistant can perform on a proof is to check its correctness. This participates in the quest of a new step in mathematical rigor: the point where nothing is understated, and where the reader can therefore be replaced by a program. This quest for rigor is specially important for the large proofs, either hand written or computer aided, that mathematicians have built since the middle of the XXth century. For instance, without using a proof assistant, it is quite difficult to establish the correctness of a proofs using symbolic computations on polynomials formed with hundreds of monomials, or a case analysis requiring the inspection of several hundreds of cases, or establishing that a complex object such as a long program or a complex digital circuit has some property. This quest for correctness is especially important in application domains where a malfunction may jeopardize human life, health or environment, such as transportations or computer aided surgery.
Besides this correctness check, proof assistants can help the users to build proofs interactively. The ``tactic language'' allowing the user to control the system in this proof construction process has always been the object of intensive studies. The ML language, for instance, was originally the tactic language of the LCF proof assistant. More recent questions about this language are focused on the formal expression of its operational semantic, in particular the handling of exceptions.
Proof assistants may also prove some easy lemmas automatically, transform mathematical proofs into other formal objects such as programs.
A more recent kind of applications is the construction of large libraries of mathematical results on the net.
