14
$\begingroup$

I'm a theoretical computer scientist and my research is focused mainly on structural and algorithmic graph theory. Recently I've been very interested in using proof assistants.

As a "pet project" to get things started, I thought I'd try to formalize some classical results in graph theory (and maybe other areas I dabble in like recursion theory and computational complexity theory). Since I'm new to this, I'd like some advice. What mathematical topics should I learn in order to get proficient in proof assistants? Type theory? Category theory? Also, as a beginner, which proof assistant is more suitable for me? Coq? Lean? I'd appreciate your help.

Improve this question
$\endgroup$
2

4 Answers 4

Reset to default
7
$\begingroup$

I came to proof assistants from TCS about a year ago, so perhaps I am well placed to answer your question. This may be somewhat opinion-based, but I don't feel it is necessary to learn category theory before learning about proof assistants - category theory is only one mathematical subject, and although it is relevant to some lower-level concepts, you will mostly not need it to work on higher-level subjects such as graph theory. I myself have only a superficial understanding of category theory, but I have still been able to formalize a lot of mathematics.

I would say type theory will be useful to understand, since the programming languages you mentioned are based on it. I found Type Theory and Functional Programming by Simon Thompson had a good introductory chapter on this.

Improve this answer
$\endgroup$
5
  • 1
    $\begingroup$ What gave you the impression one needs category theory to use proof assistants, if I may ask? $\endgroup$
    – Andrej Bauer
    Commented Feb 14, 2022 at 20:46
  • $\begingroup$ @AndrejBauer I think one reason people feel these are connected is that proof assistants use monads, a concept from category theory. $\endgroup$
    – Bolton Bailey
    Commented Feb 14, 2022 at 20:50
  • 1
    $\begingroup$ For example, if you want to program a tactic in Lean, you will need to use the tactic monad. But I would say if you want to do this, just learn about monads - it's not necessary to learn category theory beyond that. $\endgroup$
    – Bolton Bailey
    Commented Feb 14, 2022 at 20:53
  • 2
    $\begingroup$ I see. Monads as a programming technique are indeed based on the category-theoretic monads, but one does not really need the latter to learn the former, as witnessed by scores of competent Haskell programmers who know almost no category theory. $\endgroup$
    – Andrej Bauer
    Commented Feb 14, 2022 at 20:57
  • 1
    $\begingroup$ @AndrejBauer There's no particular reason. Maybe just because lots of people I know of that use proof assistants are well versed in category theory. $\endgroup$
    – Rafael Coelho
    Commented Feb 14, 2022 at 22:15
6
$\begingroup$

I would say the most confusing (and often frustrating) notion for many first users is that types are not sets, so unless you plan on using a proof assistant specifically based on set theory (almost all proof assistants are in some way based on type theory), you need to understand the difference between types and sets.

Here are a few pointers I like to keep in mind:

  • Types are syntactic approximations of sets. This means:

    • We distinguish between types (sets) and terms (elements), so you cannot have a type of types. Instead, you can have a type indexed family of types

  • There are often two kinds of equalities:

    • definitional (syntactic) equality: can be computed by examining the terms (ie. $1 + 2 \equiv 3$)
    • semantic equality: the usual "mathematical" equality (ie. $n + m = m + n$)
    • definitional equality always implies semantic equality, but not conversely

  • Usually, there are no quotient types.

  • Usually, there are no subtypes. However there are often ways of getting around this:

    • A subtype of $A$ can be specified as a predicate $\phi : A\to\text{Prop}$
    • A subtype of $A$ can be specified as a sigma type: $\Sigma_{x : A}\phi(x)$, where $\phi : A\to\text{Prop}$. However, elements of sigma types are pairs $(x,\rho)$, where $\rho$ is a proof of $\phi(x)$.
    • Some proof assistants offer a form of typeclass mechanism for mathematical structures (ie. a ring is also group)

  • You may often need the function extensionality axiom to show that pointwise equal functions are equal

  • Some proof assistants may offer limited support for quotients and subtypes by sacrificing computational properties.

Improve this answer
$\endgroup$
4
$\begingroup$

Here are some topics I would recommend learning:

  • Some Functional Programming. I think it is good to learn some functional programming language. Preferably some language which takes immutability seriously and has a rich type system. Most popular proof assistants are based on some kind of functional programming environment, so this should help you get into the ecosystem. It is also good to understand some concepts like Algebraic Data Types.
  • Some introductory formal logic. Many mathematicians tend to understand proofs intuitively and for them proofs are not exactly mathematical objects but the instruments they use to study mathematics with. A first course in formal logic will teach you how to work with proofs themselves. I would suggest learning some topics like proof systems, soundness, completeness, decidability.

The rest is optional. You do not need to learn Category Theory or Type theory to get started. These theories are essential to understands the deep topics involving logic, but it is not essential for just using the assistants. At this point, it is best to start with a Proof Assistant textbook like Software Foundations instead.

Improve this answer
$\endgroup$
3
$\begingroup$

Unlike the other answers, I'm fairly convinced you do not need to learn anything (category theory, type theory, functional programming, or even logic) before hand. I have two basic reasons for this. First, empirically it seems that a number of undergraduate students pick up proof assistants without formal training in those subjects. Second, a good textbook, video series, course, or tutorial for your proof assistant should cover what you need of those topics.

Certainly after you learn a proof assistant you will be better acquainted with logic (especially that used by the proof assistant), with type theory (if it uses HOL of DTT), and with functional programming (again, if it is type theory based or is implemented directly in OCaml via the LCF approach). Also, you will probably develop a natural curiosity about those subjects, as well as category theory, and this is great! (I've suggested actually that one of the best way to learn type theory is to learn a proof assistant.) But they are not a prerequisite IMHO.

In particular I'm worried about sending folks to take full courses in logic (model theory, the completeness theorems), functional programming (building a Scheme interpreter inside Scheme), type theory (strong normalization), and category theory (adjoint functors) before at least trying their hand at a proof assistant.

If you are interested in Lean (and there are lots of great alternatives!), the natural number game is a great place to start. After that, see the recommended next steps here. But notice none of the recommendations on that page say to learn other things first (although one of the possible recommendations is an undergraduate logic course which is taught alongside Lean).

My personal story: I did happen to know logic and some BASIC programming before starting on proof assistants. But I learned functional programming and type theory through the HOL Light proof assistant tutorial, and dependent type theory though the Lean tutorial. I even learned about type classes and monads through Lean.

Improve this answer
$\endgroup$
0

Not the answer you're looking for? Browse other questions tagged or ask your own question.