Chapter 1
Introduction

My first contact with the ideas of formalised mathematics came from reading the anonymously authored QED Manifesto [Ano94[Ano94]AnonymousThe QED manifesto (1994)Automated Deduction--CADEhttp://www.cse.chalmers.se/research/group/logic/TypesSS05/Extra/wiedijk_2.pdf]In this thesis, shortened citation references will appear in the sidebar, a full bibliography with all reference details is provided at the end of the document. Some sidebar citations will be omitted if there is not enough space. which envisions a 'QED system' in which all mathematical knowledge is stored in a single, computer-verified repository. This idea dizzied me: perhaps review of mathematics will amount to remarking on style and interest, with checking of proofs performed automatically from a machine readable document.

The general term that I will use for software that works towards this vision is proof assistant or Interactive Theorem Prover ITP. A proof assistant at its most general is a piece of software that allows users to create and verify mathematical proofs. In Section 2.1 I will provide more detail how proof assistants are generally constructed.

In 2007, Freek Wiedijk [Wie07[Wie07]Wiedijk, FreekThe QED manifesto revisited (2007)Studies in Logic, Grammar and Rhetorichttp://www.cs.ru.nl/~freek/pubs/qed2.pdf] pronounced the QED project to have "not been a success (yet)", citing not enough people working on formalised mathematics and the severe differences between formalised and 'real' mathematics, both at a syntactic level (formalised mathematics resembles source code) and at a foundational level (formalised mathematics is usually constructive and procedural as opposed to classical and declarative). Similarly, Alan Bundy [Bun11[Bun11]Bundy, AlanAutomated theorem provers: a practical tool for the working mathematician? (2011)Annals of Mathematics and Artificial Intelligencehttps://doi.org/10.1007/s10472-011-9248-8] notes that although mathematicians have readily adopted computational tools such as [Knu86[Knu86]Knuth, Donald E.The TeXbook (1986)publisher Addison-Wesley] and computer algebra systemsA computer algebra system (CAS) is a tool for symbolic manipulation of formulae and expressions, without necessarily having a formalised proof that the manipulation is sound. Examples of CASes include Maple and Mathematica., computer aided proving has had very little impact on the workflow of a working mathematician. Bundy cites several reasons for this which will be discussed in Section 1.1.

Now, a decade later, the tide may be turning. In 2021, proof assistants are pretty good. There are several well-supported large-scale systems such as Isabelle [Pau89], Coq [Coq], Lean [MKA+15], HOL Light [Har09], Agda [Nor08], Mizar [GKN15], PVS [SORS01] and many more. These systems are used to define and prove mathematical facts in a variety of logics (e.g. FOL, HOL, CIC, univalent foundations). These systems are bridged to powerful, automated reasoning systems (e.g. Vampire [RV02], Z3 [MB08], E [SCV19] and Leo-III [SB18a]. Within these systems, many theorems big and small (4-colour theorem [Gon08], Feit-Thompson theorem [GAA+13], Kepler conjecture [HAB+17]) have been proved in a variety of fields, accompanied by large mathematical libraries (Isabelle's Archive of Formal Proofs, Lean's mathlib, Coq's Mathematical Components, Mizar's Formalized Mathematics) whose intersection with undergraduate and research level mathematics is steadily growingSee, for example, the rate of growth of the Lean 3 mathematical library https://leanprover-community.github.io/mathlib_stats.html..

However, in spite of these advances, we are still yet to see widespread adoption of ITP by mathematicians outside of some (growing) cliques of enthusiasts. In this thesis I wish to address this problem through engaging with how mathematicians use and understand proofs to create new ways of interacting with formalised proof. Let's first expand on the problem a little more and then use this to frame the research questions that I will tackle for the remainder of the thesis.

1.1. Mathematicians and proof assistants

Here I offer 3 possible explanations for why mathematicians have not adopted proof assistants. Many have commented on these before: Bundy [Bun11] summarises the main challenges well.

1. Differing attitudes towards correctness and errors. Mathematicians don't worry about mistakes in the same way as proof assistants doI will present some evidence for this in Section 2.5.. Mathematicians care deeply about correctness, but historically the dynamics determining whether a result is considered to be true are also driven by sociological mechanisms such as peer-review; informal correspondences; 'folk' lemmas and principles; reputation of authors; and so on [MUP79[MUP79]de Millo, Richard A; Upton, Richard J; Perlis, Alan JSocial processes and proofs of theorems and programs (1979)Communications of the ACMhttps://doi.org/10.1145/359104.359106]. A proxy for trustworthiness of a result is the number of other mathematicians that have scrutinized the work. That is, if the proof is found on an undergraduate curriculum, you can predict with a high degree of confidence that any errors in the proof will be brought to the lecturer's attention. In contrast, a standalone paper that has not yet been used for any subsequent work by others is typically treated with some degree of caution.

2. High cost. Becoming proficient in an ITP system such as Isabelle or Coq can require a lot of time. And then formalising an area of maths can take around ten times the amount of time required to write a corresponding paper or textbook on the topic. This time quickly balloons if it is also necessary to write any underlying assumed knowledge of the topic (e.g., measure theory first requires real analysis). This 'loss factor' of the space cost of developing a formalised proof over that of a natural language proof was first noted by de Bruijn in relation to his AUTOMATH prover [DeB80[DeB80]De Bruijn, Nicolaas GovertA survey of the project AUTOMATH (1980)To H.B.Curry: Essays on Combinatory Logic,Lambda Calculus and Formalismhttps://research.tue.nl/files/2092478/597605.pdf]. De Bruijn estimates a factor of 20 for AUTOMATH, and Wiedijk later estimates this factor to be closer to three or four in Mizar [Wie00[Wie00]Wiedijk, FreekThe de Bruijn Factor (2000)http://www.cs.ru.nl/F.Wiedijk/factor/factor.pdf]. There are costs other than space too, the main one of concern here being the time to learn to use the tools and the amount of work required per proof.

3. Low reward. What does a mathematician have to gain from formalising their research? In many cases, there is little to gain other than confirming something the researcher knew to be true anyway. The process of formalisation may bring to light 'bugs' in the work: perhaps there is a trivial case that wasn't accounted for or an assumption needs to be strengthened. Sometimes the reward is high enough that there is a clear case for formalisation, particularly when the proof involves some computer-generated component. This is exemplified by Hales' proof [Hal05[Hal05]Hales, Thomas CA proof of the Kepler conjecture (2005)Annals of mathematicshttp://annals.math.princeton.edu/wp-content/uploads/annals-v162-n3-p01.pdf] and later formalised proof [HAB+17[HAB+17]Hales, Thomas C; Adams, Mark; Bauer, Gertrud; et al.A formal proof of the Kepler conjecture (2017)Forum of Mathematics, Pihttps://doi.org/doi:10.1017/fmp.2017.1] of the Kepler conjecture. The original proof involved lengthy computer generated steps that were difficult for humans to check, and so Hales led the Flyspeck project to formalise it, taking 21 collaborators around a decade to complete. Another celebrated example is Gonthier's formalisation of the computer-generated proof of the four-colour theorem [Gon08[Gon08]Gonthier, GeorgesFormal proof--the four-color theorem (2008)Notices of the AMShttps://www.ams.org/notices/200811/tx081101382p.pdf]. Formalisation is also used regularly in formalising expensive hardware and safety-critical computer software (e.g., [KEH+09[KEH+09]Klein, Gerwin; Elphinstone, Kevin; Heiser, Gernot; et al.seL4: Formal verification of an OS kernel (2009)Proceedings of the ACM SIGOPS 22nd symposium on Operating systems principleshttps://doi.org/10.1145/1629575.1629596, Pau98[Pau98]Paulson, Lawrence CThe inductive approach to verifying cryptographic protocols (1998)Journal of Computer Securityhttp://content.iospress.com/articles/journal-of-computer-security/jcs102]).

The economics of the matter are such that the gains of using ITP are too low compared to the benefits for the majority of cases. Indeed, since mathematicians have a different attitude to correctness, there are sometimes no benefits to formalisation. As ITP developers, we can improve the situation by either decreasing the learning cost or increasing the utility.

How can we make ITP easier to learn? One way is to teach it in undergraduate mathematics curricula (not just computer science). An example of such a course is Massot's Introduction aux mathématiques formalisées taught at the Université Paris Sud. Another way is to improve the usability of the user interface for the proof assistant; I will consider this point in more detail in Chapter 5.

How can we increase the utility that mathematicians gain from using a proof assistant? In this thesis I will argue that one way to help with these three issues is to put more emphasis on interactive theorem provers providing explanations rather than a mere guarantee of correctness. We can see that explanations are important because mathematicians care about new proofs of old results that treat the problem in a new way. Proofs from the Book [AZHE10[AZHE10]Aigner, Martin; Ziegler, Günter M; Hofmann, Karl H; et al.Proofs from the Book (2010)publisher Springerhttps://doi.org/10.1007/978-3-662-57265-8] catalogues some particularly lovely examples of this.

Can computers also provide informal proofs with more emphasis on explanations? Gowers [Gow10[Gow10]Gowers, W. T.Rough structure and classification (2010)Visions in Mathematicshttps://www.dpmms.cam.ac.uk/~wtg10/gafavisions.ps §2] presents an imagined interaction between a mathematician and a proof assistant of the future.

Quotation 1.1

Excerpt from an imagined conversation between a mathematician and a computer from [Gow10 §2].

Mathematician. Is the following true? Let . Then for sufficiently large, every set of size at least contains a subset of the form ?

Computer. Yes. If is non-empty, choose and set .

M. All right all right, but what if is not allowed to be zero?

C. Have you tried induction on , with some tending to zero?

M. That idea is no help at all. Give me some examples please.

C. The obvious greedy algorithm gives the set

An interesting feature of this conversation is that the status of the formal correctness of any of the statements conveyed by the computer is not mentioned. Similar notions are brought to light in the work of Corneli et al. [CMM+17[CMM+17]Corneli, Joseph; Martin, Ursula; Murray-Rust, Dave; et al.Modelling the way mathematics is actually done (2017)Proceedings of the 5th ACM SIGPLAN International Workshop on Functional Art, Music, Modeling, and Designhttps://doi.org/10.1145/3122938.3122942] in their modelling of informal mathematical dialogues and exposition.

Why not have both explanatory and verified proofs? I suspect that if an ITP system is to be broadly adopted by mathematicians, it must concisely express theorems and their proofs in a way similar to that which a mathematician would communicate with fellow mathematicians. This not only requires constructing human-readable explanations, but also a reimagining of how the user can interact with the prover.

In this thesis, I will focus on problems that are considered 'routine' for a mathematician. That is, problems that a mathematician would typically do 'on autopilot' or by 'following their nose' For example, showing that from the ring axioms.. I choose to focus on this class of problem because I believe it is an area where ITP could produce proofs that explain why they are true rather than merely provide a certificate of correctness. The typical workflow when faced with a problem like this is to either meticulously provide a low-level proof or apply automation such as Isabelle's auto, or an automation orchestration tool such as Isabelle's Sledgehammer [BN10[BN10]Böhme, Sascha; Nipkow, TobiasSledgehammer: judgement day (2010)International Joint Conference on Automated Reasoninghttps://doi.org/10.1007/978-3-642-14203-1_9]. In the case of using an automation tacticBroadly, a tactic is a program for creating proofs. I will drill down on how this works in Chapter 2. like auto the tactic will either fail or succeed, leaving the user with little feedback on why the result is true. There are some tools for producing intelligible proofs from formalised ones, for example, the creation of Isar [Wen99[Wen99]Wenzel, MarkusIsar - A Generic Interpretative Approach to Readable Formal Proof Documents (1999)Theorem Proving in Higher Order Logicshttps://doi.org/10.1007/3-540-48256-3_12] proofs from Sledgehammer by Blanchette et al. [BBF+16[BBF+16]Blanchette, Jasmin Christian; Böhme, Sascha; Fleury, Mathias; et al.Semi-intelligible Isar proofs from machine-generated proofs (2016)Journal of Automated Reasoninghttps://doi.org/10.1007/s10817-015-9335-3]. However, gaining an intuition for a proof will be easier if the proof is generated in a way that reflects how a human would solve the problem, and so translating a machine proof to a proof which a human will extract meaning from is an uphill battle.

1.1.1. Types of understandability

The primary motivation of the work in this thesis is to help make ITP systems more appealing to mathematicians. The approach I chosen to take towards this is to research ways of making ITP systems more understandable. There are many components of ITP that I consider with respect to understandability:

The different parts of my thesis will address different sets of these ways in which a proof assistant can be understandable. With respect to the automation and underlying-representation aspects of understandability, we will see in Section 2.6 that there is some debate over whether prover automation needs to be easy to follow for a human or not (machine-like vs. human-like). In this thesis I take a pragmatic stance that the understandability of automation and underlying-representation need not be human-like provided that the resulting interaction and output is understandable. However, as I investigate in Chapter 4, there may be ways of creating automation that are more conducive to creating understandable output and interaction.

1.2. Research questions

In the context of these facets of an understandable ITP system, there arise some key research questions that I seek to study.

Question 1. What constitutes a human-like, understandable proof?

Objectives:

Question 2. How can human-like reasoning be represented within an interactive theorem prover to produce formalised, understandable proofs?

Objectives:

Question 3. How can this mode of human-like reasoning be presented to the user in an interactive, multimodal way?

Objectives:

1.3. Contributions

This thesis presents a number of contributions towards the above research questions:

  1. An abstract calculus for developing human-like proofs (Chapter 3).

  2. An interface between this abstraction layer and a metavariable-driven tactic state, as is used in theorem provers such as Coq and Lean, producing formally verified proofs (Chapter 3 and Appendix A).

  3. A procedure for generating natural language proofs from this calculus (Section 3.6).

  4. The 'subtasks' algorithm, a system for automating the creation of chains of equalities and inequalities. This work has been published in [AGJ19[AGJ19]Ayers, E. W.; Gowers, W. T.; Jamnik, MatejaA human-oriented term rewriting system (2019)KI 2019: Advances in Artificial Intelligence - 42nd German Conference on AIhttps://www.repository.cam.ac.uk/bitstream/handle/1810/298199/main.pdf?sequence=1] (Chapter 4).

  5. A graphical user interface framework for interactive theorem provers (Chapter 5). This has been published in [AJG21[AJG21]Ayers, E. W.; Jamnik, Mateja; Gowers, W. T.A graphical user interface framework for formal verification (2021)Interactive Theorem Provinghttps://doi.org/10.4230/LIPIcs.ITP.2021.4].

  6. An implementation of all of the above contributions in the Lean 3 theorem prover.

  7. A study assessing the impact of natural language proofs with practising mathematicians (Chapter 6).

The implementations for these contributions can be found at the following links:

1.4. Structure of this document

In Chapter 2, I will provide an overview of the background material needed for the remaining chapters. Next, in Chapter 3, I introduce the HumanProof software for producing human-like proofs within the Lean proof assistant. I provide motivation of the design in Section 3.1, an overview of the system in Section 3.2 and then dive in to the details of how the system is designed, including the natural-language generation engine in Section 3.6. Chapter 4 discusses a system for producing equational reasoning proofs called the subtask algorithm. Chapter 5 details the ProofWidgets system, which is used to produce the user interface of HumanProof. Chapter 6 provides the design and results of a user study that I conducted on mathematicians to determine whether HumanProof really does provide understandable proofs. Finally, Chapter 7 wraps things up with some reflection on my progress and a look ahead to future work.

There are also four appendices:

1.5. Previously published work and collaboration

The work in Chapter 3 is my own, although the box calculus presented is inspired through many sessions of discussion with W.T. Gowers and the design of Gowers' previous collaboration with Ganesalingam [GG17[GG17]Ganesalingam, Mohan; Gowers, W. T.A fully automatic theorem prover with human-style output (2017)Journal of Automated Reasoninghttps://doi.org/10.1007/s10817-016-9377-1]. More on this will be given when it is surveyed in Section 2.6 and Section 3.3.5.

The work in Chapter 4 is previously published at KI 2019 [AGJ19[AGJ19]Ayers, E. W.; Gowers, W. T.; Jamnik, MatejaA human-oriented term rewriting system (2019)KI 2019: Advances in Artificial Intelligence - 42nd German Conference on AIhttps://www.repository.cam.ac.uk/bitstream/handle/1810/298199/main.pdf?sequence=1].

The work presented in Chapter 5 is pending publication in ITP 2021 [AJG21[AJG21]Ayers, E. W.; Jamnik, Mateja; Gowers, W. T.A graphical user interface framework for formal verification (2021)Interactive Theorem Provinghttps://doi.org/10.4230/LIPIcs.ITP.2021.4] and is also merged in to the Lean 3 community repository. The design is strongly influenced by Elm and React; however, there are a number of novel architectural contributions necessitated by the unique challenges of implementing a portable framework within a proof assistant.

The user study presented in Chapter 6 is all my own work with a lot of advisory help from Mateja Jamnik, Gem Stapleton and Aaron Stockdill on designing the study.

1.6. Acknowledgements

I thank my supervisors W. T. Gowers and Mateja Jamnik for their ideas, encouragement and support and for letting me work on such a wacky topic. I thank Gabriel Ebner and Brian Gin-ge Chen for reading through my ProofWidgets PRs. I thank Patrick Massot, Kevin Buzzard and the rest of the Lean Prover community for complaining about my PRs after the fact. I thank Jeremy Avigad for taking the time to introduce me to Lean at the Big Proof conference back in 2017. I thank Bohua Zhan, Chris Sangwin, and Makarius Wenzel and many more for the enlightening conversations on automation for mathematicians at Big Proof and beyond. I thank Peter Koepke for being so generous in inviting me to Bonn to investigate Naproche/SAD with Steffan Frerix and Andrei Paskevich. I thank Larry Paulson and the ALEXANDRIA team for letting me crash their weekly meetings. I thank my parents for letting me write up in the house during lockdown.

I thank my friends and colleagues in the CMS. Andrew, Eric, Sammy P, Sven, Ferdia, Mithuna, Kasia, Sam O-T, Bhavik, Wojciech, and many more. In parallel, the Computer Laboratory: Chaitanya, Botty, Duo, Daniel, Aaron, Angeliki, Yiannos, Wenda, Zoreh.

This research was supported by EPSRC and the Cantab Capital Institute for the Mathematics of Information.

1.6.1. Typesetting acknowledgements

I decided to typeset this thesis as HTML-first, print second. The digital copy may be found at https://edayers.com/thesis. The printed version of this thesis was generated by printing out the website version and concatenating.

I was able to create the thesis in this way thanks to many open-source projects. I will acknowledge the main ones here. React, Gatsby, Tachyons, PrismJS. Thanks to Titus Woormer for remarkJS and also adding my feature request in less than 24 hours! The code font is PragmataPro created by Fabrizio Schiavi. The style of the site is a modified version of the Edward Tufte Handout style. The syntax colouring style is based on the VS theme by Andrew Lock. I also use some of the vscode-icons icons.

Bibliography for this chapter

  • [AGJ19]Ayers, E. W.; Gowers, W. T.; Jamnik, MatejaA human-oriented term rewriting system (2019)KI 2019: Advances in Artificial Intelligence - 42nd German Conference on AIvolume 11793pages 76--86editors Benzmüller, Christoph; Stuckenschmidt, Heinerorganization Springerpublisher Springerdoi 10.1007/978-3-030-30179-8_6https://www.repository.cam.ac.uk/bitstream/handle/1810/298199/main.pdf?sequence=1
  • [AJG21]Ayers, E. W.; Jamnik, Mateja; Gowers, W. T.A graphical user interface framework for formal verification (2021)Interactive Theorem Provingvolume 193pages 4:1--4:16editors Cohen, Liron; Kaliszyk, Cezarypublisher Schloss Dagstuhl - Leibniz-Zentrum für Informatikdoi 10.4230/LIPIcs.ITP.2021.4https://doi.org/10.4230/LIPIcs.ITP.2021.4
  • [Ano94]AnonymousThe QED manifesto (1994)Automated Deduction--CADEvolume 12pages 238--251http://www.cse.chalmers.se/research/group/logic/TypesSS05/Extra/wiedijk_2.pdfUnofficially credited as Robert Boyer
  • [AZHE10]Aigner, Martin; Ziegler, Günter M; Hofmann, Karl H; Erdos, PaulProofs from the Book (2010)publisher Springerisbn 978-3-662-57264-1https://doi.org/10.1007/978-3-662-57265-8
  • [BBF+16]Blanchette, Jasmin Christian; Böhme, Sascha; Fleury, Mathias; Smolka, Steffen Juilf; Steckermeier, AlbertSemi-intelligible Isar proofs from machine-generated proofs (2016)Journal of Automated Reasoningvolume 56number 2pages 155--200publisher Springerdoi 10.1007/s10817-015-9335-3https://doi.org/10.1007/s10817-015-9335-3
  • [BN10]Böhme, Sascha; Nipkow, TobiasSledgehammer: judgement day (2010)International Joint Conference on Automated Reasoningpages 107--121editors Giesl, Jürgen; Hähnle, Reinerorganization Springerdoi 10.1007/978-3-642-14203-1_9https://doi.org/10.1007/978-3-642-14203-1_9
  • [Bun11]Bundy, AlanAutomated theorem provers: a practical tool for the working mathematician? (2011)Annals of Mathematics and Artificial Intelligencevolume 61number 1pages 3--14doi 10.1007/s10472-011-9248-8https://doi.org/10.1007/s10472-011-9248-8
  • [CMM+17]Corneli, Joseph; Martin, Ursula; Murray-Rust, Dave; Pease, Alison; Puzio, Raymond; Rino Nesin, GabrielaModelling the way mathematics is actually done (2017)Proceedings of the 5th ACM SIGPLAN International Workshop on Functional Art, Music, Modeling, and Designpages 10--19editors Sperber, Michael; Bresson, Jeanorganization ACMpublisher ACMdoi 10.1145/3122938.3122942https://doi.org/10.1145/3122938.3122942
  • [Coq]The Coq Development TeamThe Coq Reference Manual (2021)https://coq.inria.fr/distrib/current/refman/#
  • [DeB80]De Bruijn, Nicolaas GovertA survey of the project AUTOMATH (1980)To H.B.Curry: Essays on Combinatory Logic,Lambda Calculus and Formalismpages 579-606editors Hindley, J.R.; Seldin, J.P.publisher Academic Presshttps://research.tue.nl/files/2092478/597605.pdf
  • [GAA+13]Gonthier, Georges; Asperti, Andrea; Avigad, Jeremy; Bertot, Yves; Cohen, Cyril; Garillot, François; Le Roux, Stéphane; Mahboubi, Assia; O’Connor, Russell; Biha, Sidi Ould; othersA machine-checked proof of the odd order theorem (2013)International Conference on Interactive Theorem Provingpages 163--179organization Springerhttps://hal.inria.fr/docs/00/81/66/99/PDF/main.pdf
  • [GG17]Ganesalingam, Mohan; Gowers, W. T.A fully automatic theorem prover with human-style output (2017)Journal of Automated Reasoningvolume 58number 2pages 253--291doi 10.1007/s10817-016-9377-1https://doi.org/10.1007/s10817-016-9377-1
  • [GKN15]Grabowski, Adam; Korniłowicz, Artur; Naumowicz, AdamFour decades of Mizar (2015)Journal of Automated Reasoningvolume 55number 3pages 191--198editors Trybulec, Andrzej; Trybulec Kuperberg, Krystynapublisher Springerdoi 10.1007/s10817-015-9345-1https://doi.org/10.1007/s10817-015-9345-1
  • [Gon08]Gonthier, GeorgesFormal proof--the four-color theorem (2008)Notices of the AMSvolume 55number 11pages 1382--1393editor Magid, Andyhttps://www.ams.org/notices/200811/tx081101382p.pdf
  • [Gow10]Gowers, W. T.Rough structure and classification (2010)Visions in Mathematicspages 79--117publisher Springerhttps://www.dpmms.cam.ac.uk/~wtg10/gafavisions.ps
  • [HAB+17]Hales, Thomas C; Adams, Mark; Bauer, Gertrud; Dang, Dat Tat; Harrison, John; Hoang, Truong Le; Kaliszyk, Cezary; Magron, Victor; McLaughlin, Sean; Nguyen, Thang Tat; Nguyen, Truong Quang; Nipkow, Tobias; Obua, Steven; Pleso, Joseph; Rute, Jason M.; Solovyev, Alexey; Ta, An Hoai Thi; Tran, Trung Nam; Trieu, Diep Thi; Urban, Josef; Vu, Ky Khac; Zumkeller, RolandA formal proof of the Kepler conjecture (2017)Forum of Mathematics, Pivolume 5organization Cambridge University Pressdoi doi:10.1017/fmp.2017.1https://doi.org/doi:10.1017/fmp.2017.1
  • [Hal05]Hales, Thomas CA proof of the Kepler conjecture (2005)Annals of mathematicspages 1065--1185publisher Mathematics Department, Princeton Universityhttp://annals.math.princeton.edu/wp-content/uploads/annals-v162-n3-p01.pdf
  • [Har09]Harrison, JohnHOL Light: An Overview. (2009)TPHOLsvolume 5674pages 60--66editors Berghofer, Stefan; Nipkow, Tobias; Urban, Christian; et al.organization Springerdoi 10.1007/978-3-642-03359-9_4https://doi.org/10.1007/978-3-642-03359-9_4
  • [KEH+09]Klein, Gerwin; Elphinstone, Kevin; Heiser, Gernot; Andronick, June; Cock, David; Derrin, Philip; Elkaduwe, Dhammika; Engelhardt, Kai; Kolanski, Rafal; Norrish, Michael; Sewell, Thomas; Tuch, Harvey; Winwood, SimonseL4: Formal verification of an OS kernel (2009)Proceedings of the ACM SIGOPS 22nd symposium on Operating systems principlespages 207--220editors Matthews, Jeanna Neefe; Anderson, Thomas E.organization ACMdoi 10.1145/1629575.1629596https://doi.org/10.1145/1629575.1629596
  • [Knu86]Knuth, Donald E.The TeXbook (1986)publisher Addison-Wesleyisbn 0-201-13447-0
  • [MB08]de Moura, Leonardo; Bjørner, NikolajZ3: An efficient SMT solver (2008)International conference on Tools and Algorithms for the Construction and Analysis of Systemspages 337--340editors Ramakrishnan, C. R.; Rehof, Jakoborganization Springerdoi 10.1007/978-3-540-78800-3_24https://doi.org/10.1007/978-3-540-78800-3_24
  • [MKA+15]de Moura, Leonardo; Kong, Soonho; Avigad, Jeremy; Van Doorn, Floris; von Raumer, JakobThe Lean theorem prover (system description) (2015)International Conference on Automated Deductionvolume 9195pages 378--388editors Felty, Amy P.; Middeldorp, Aartorganization Springerdoi 10.1007/978-3-319-21401-6_26https://doi.org/10.1007/978-3-319-21401-6_26
  • [MUP79]de Millo, Richard A; Upton, Richard J; Perlis, Alan JSocial processes and proofs of theorems and programs (1979)Communications of the ACMvolume 22number 5pages 271--280doi 10.1145/359104.359106https://doi.org/10.1145/359104.359106
  • [Nor08]Norell, UlfDependently typed programming in Agda (2008)International school on advanced functional programmingvolume 5832pages 230--266editors Koopman, Pieter W. M.; Plasmeijer, Rinus; Swierstra, S. Doaitseorganization Springerdoi 10.1007/978-3-642-04652-0_5https://doi.org/10.1007/978-3-642-04652-0_5
  • [Pau89]Paulson, Lawrence CThe foundation of a generic theorem prover (1989)Journal of Automated Reasoningvolume 5number 3pages 363--397doi 10.1007/BF00248324https://doi.org/10.1007/BF00248324
  • [Pau98]Paulson, Lawrence CThe inductive approach to verifying cryptographic protocols (1998)Journal of Computer Securityvolume 6number 1-2pages 85--128http://content.iospress.com/articles/journal-of-computer-security/jcs102
  • [RV02]Riazanov, Alexandre; Voronkov, AndreiThe design and implementation of VAMPIRE (2002)AI communicationsvolume 15number 2-3pages 91--110http://content.iospress.com/articles/ai-communications/aic259
  • [SB18a]Steen, Alexander; Benzmüller, ChristophThe higher-order prover Leo-III (2018)International Joint Conference on Automated Reasoningvolume 10900pages 108--116editors Galmiche, Didier; Schulz, Stephan; Sebastiani, Robertopublisher Springerdoi 10.1007/978-3-319-94205-6_8https://doi.org/10.1007/978-3-319-94205-6_8
  • [SCV19]Schulz, Stephan; Cruanes, Simon; Vukmirović, PetarFaster, Higher, Stronger: E 2.3 (2019)Proc. of the 27th CADE, Natal, Brasilnumber 11716pages 495--507editor Fontaine, Pascalpublisher Springerhttp://wwwlehre.dhbw-stuttgart.de/~sschulz/bibliography.html#SCV:CADE-2019
  • [SORS01]Shankar, Natarajan; Owre, Sam; Rushby, John M; Stringer-Calvert, Dave WJPVS prover guide (2001)Computer Science Laboratory, SRI International, Menlo Park, CAhttps://pvs.csl.sri.com/doc/pvs-prover-guide.pdf
  • [Wen99]Wenzel, MarkusIsar - A Generic Interpretative Approach to Readable Formal Proof Documents (1999)Theorem Proving in Higher Order Logicsvolume 1690pages 167--184editors Bertot, Yves; Dowek, Gilles; Hirschowitz, André; et al.publisher Springerdoi 10.1007/3-540-48256-3_12https://doi.org/10.1007/3-540-48256-3_12
  • [Wie00]Wiedijk, FreekThe de Bruijn Factor (2000)http://www.cs.ru.nl/F.Wiedijk/factor/factor.pdf
  • [Wie07]Wiedijk, FreekThe QED manifesto revisited (2007)Studies in Logic, Grammar and Rhetoricvolume 10number 23pages 121--133http://www.cs.ru.nl/~freek/pubs/qed2.pdf