How would you explain so a beginner in simple terms why Proof Assistants are important, and how / why they are used?
In mathematics, I believe they're important for the following reasons:
They might change the way we teach. There are plenty of computer tools for teaching at school level but a proof assistant offers something different; for the student beginning to learn rigorous analysis (epsilon-delta etc) these systems will, I believe (once we've made them more user-friendly), have the potential to help to show undergraduates what we mathematicians mean by a proof. Current status at the time of writing: the systems are too intimidating to use and to learn for someone who is just beginning to learn epsilon-delta analysis, so work must be done to make them more friendly to beginners.
They might change the way we communicate mathematics. Right now, as Patrick Massot points out, it is the author of a paper who chooses how much detail to use when explaining their ideas. In the future one could imagine a web-based document where, if a reader without the required background is stuck somewhere, they could "zoom in" and see more details of the argument, theoretically even down to the axioms. Current state of things: Alectryon is being developed for Lean 4 and this should play a role; it will need to be integrated with earlier work of Massot.
They might change the way we do research, in several ways. For example a PhD student, when trying to figure out if a statement in algebraic geometry is true or not, might be able to search an online database of statements in algebraic geometry, or ask a tactic to try and prove or disprove their statement by either database search or a hammer technique. Another example: formalising the Clausen-Scholze work taught Commelin the theory, taught Scholze "what made the proof work", and also taught everyone a simplification to the proof (Commelin's insight that the full strength of the Breen-Deligne resolution was not required, thus removing from the proof the necessity to appeal to facts from stable homotopy theory).
2$\begingroup$ The first link isn't displayed correctly because of the extra space before "universite" (and I can't fix that myself because "Edits must be at least 6 characters" :) $\endgroup$– GraffLFeb 8, 2022 at 23:13
$\begingroup$ (this now seems to be fixed) $\endgroup$ Feb 9, 2022 at 14:23
(A lightly edited copy and paste of my answer to a similar question on the Lean Zulip chat: What is the point of Lean's maths library.)
In my talk about Lean-GPT-f at Harvard, I gave five different motivations for formalized mathematics:
- Mechanically check mathematical proofs. While it doesn’t yet make sense to have mathematicians formalize all of their work, it does make sense to formalize particularly foundational, interesting, or troublesome proofs, such as undergraduate mathematics, the independence of CH, or Scholze’s lemma in the Liquid Tensor project.
- Digitize mathematics. Everything nowadays is digitized, and systematically organized into databases. However, mathematics is remarkably resistant to this trend. Sure we have pdfs and LaTeX files of most articles, but none of these formats capture the mathematical content of the articles. Formalization of a large body of mathematics, whether the full proofs or just the theorem statements, would open up many possibilities for automatic retrieval and search of mathematics.
- Unify and archive mathematical knowledge. Right now the world of mathematics consists of a mostly disjoint collection of articles (most of them mostly true). There have been past heroic efforts from Euclid to Bourbaki to systematically organize the current mathematical knowledge of the time. More modern incarnations include Wikipedia, nLab, and the Stacks Project. Formalization provides yet another approach to this, whereby we systematically build up a library of mathematics starting at the foundations, up to the most interesting new developments.
- Prove the correctness of software and hardware. There have been some great success stories so far in software and hardware verification and I see a lot of potential for verified security software. It is also the most likely way to monetize ones skills in formal theorem proving. As the mathematics in formal libraries get more sophisticated, so do the types of algorithms that we can formalize.
- Making mathematics accessible to computers in a new way. I’ve heard it said that the one thing mathematics is good for is more mathematics. This “false truism” also holds for formalization. We don’t know the full applications of formal mathematics right now except that it will improve our ability to formalize more mathematics in the future. However, we do have hints already at the ways that one can use a large library of formal mathematics. AI projects like TacticToe, HOList, Tactician, and GPT-f are trained off of many person-years of formalization effort, and hopefully will eventually become a virtuous loop, helping users better formalize more mathematics. It’s hard to predict what we can do with a large library of formalized, computer-readable, interconnected mathematics, but it is very reasonable to believe it could have important positive future impacts on mathematics, technology, science, and education.