9
$\begingroup$

I want to learn proof based mathematics and it looks like a proof assistant like Coq and Lean could be a good way to go about verifying my proofs, without needing a PhD on hand to check through all my work. I am currently going through the natural number game and it's brilliant.

Are there any limitations or problems I may run into with my plan? I am new to proof assistants and am not sure what the limitations of such software is (I am a software engineer by trade).

$\endgroup$
3
  • 6
    $\begingroup$ So you don't have a math background? My instinct is to recommend a more traditional route. Learning to use a proof assistant is hard enough, learning mathematics at the same time seems to me like it might be too much. It's hard enough getting a proof assistant to accept a proof which you completely understand! $\endgroup$ Jul 27 at 8:32
  • $\begingroup$ Thanks @KevinBuzzard, I do not have any formal training in higher mathematics - I will try and get a book like Velleman's and go through that instead. I found the NNG really cool btw, thanks for putting that together! $\endgroup$
    – quidproquo
    Jul 27 at 17:10
  • $\begingroup$ Kevin's answer is exactly the one I would have given years ago as someone with a mathematical background who got into computer science and then logic and formal specification and proof later. However, I have worked with many colleagues with a computer science background, particularly in functional programming, who have been very successful with using proof assistants to find proofs just by interacting with the machine: they end up with proofs which they don't "completely understand", but that doesn't matter to them. Horses for courses! $\endgroup$
    – Rob Arthan
    Aug 31 at 21:59

2 Answers 2

10
$\begingroup$

I have a degree in software engineering and share the same goal as yours.

Start with Informal Proofs

Truth be told, you can learn more about proof by reading introductory maths book at university level and start writing informal proofs. A good book recommendation will be Velleman's "How to Prove It: A Structured Approach". The maths discord server is a great place to ask about your maths problem, url: https://discord.gg/math.

If you're determine on continuing this path, I can share some of my experience after learning Coq for nearly two months, especially on how writing proofs in Coq is different from writing proofs on paper.

Coq vs Other Proof Assistants

I can't comment on the differences between Coq and other proof assistants because I'm not familiar with them. But Coq and Lean might be similar because they are based on the same underlying type theory: CoC. Isabelle/HOL is based on a simpler theory instead, but they excel in producing very readable proof documents using Isar.

Maths in Coq vs Traditional Maths

  1. Proofs written in Coq are formal; proofs on paper are informal.

In programming parlance, informal proofs are pseudocodes. They're high level and written only to communicate with other mathematicians. Informal proofs are good enough as long as the other party understands what you're trying to communicate. However, you're required to fill in a lot of details by yourself.

On the other hand, formal proofs in Coq are like writing algorithms in an actual programming language. It's similar to how you'll write programs in Standard ML, OCaml or Haskell. You have to be correct down to the finest details because, now, instead of convincing an intelligent person, you have to convince Coq that your proofs are indeed correct.

  1. Coq is based on constructive type theory, while the mainstream maths are based classical set theory.

It means that you need to be familiar with both constructive type theory and classical set theory if you're going to learn maths with Coq. Why? You need to understand classical set theory to understand mainstream maths; then constructive type theory to translate those knowledge into Coq.

There are two main differences between them: (i) constructive vs classical maths, (ii) type theory vs set theory.

Classical maths is what you learn from most maths textbook (e.g. including the Velleman book I recommend above). On the other hand, constructive maths is maths done without principle of excluded middle. No proof by contradiction as well. I don't know of other subtle differences.

In set theory, new mathematical objects are always defined as sets or elements of some sets. Type theory is a bit familiar to you if you've programmed in static typed functional programming language. New mathematical objects are introduced very much like how you define new data structures in programming languages.

  1. Mastery of Coq takes time!

Don't underestimate the time and efforts needed to master your tool! You can start right away with pen and paper with informal proofs. But since you're going to write maths in Coq, you need to learn how Coq works!

  1. You may need to keep your proofs updated!

This might be surprising. Your proofs written with pen and paper won't get outdated, but your proofs written in a proof assistant will! Why? Your proofs written in proof assistants are essentially programs, so it's tied to specific versions of your proof assistant.

It means that if your proof assistant introduces breaking changes, your proofs will no longer work with the newer version of the proof assistant. A notable example is the port of mathlib from Lean 3 to Lean 4.

So, maintainability and portability across versions is a factor of consideration during your proof development. It might be no different from software development at this stage.

Connect with People

Ask for help in Coq zulip or here. People are busy, but they are friendly and welcoming. Feel free to chat with me on Coq zulip, my username there is Jiahong Lee.

Hope that my experience will be useful to you. Thanks!

$\endgroup$
4
  • $\begingroup$ Just a clarification: Agda is not based on CoC $\endgroup$
    – Couchy
    Jul 27 at 15:13
  • $\begingroup$ Thanks a lot @zacque, this is a really insightful post. I am willing to put the time in to get familiar with proof assistants (kinda treating it like a self study exercise when I have spare time). I will order the Vellemann book in the meantime. Thanks again! $\endgroup$
    – quidproquo
    Jul 27 at 17:49
  • $\begingroup$ @quidproquo Glad that it helps! I'm happy to find someone with similar interest =D $\endgroup$
    – zacque
    Jul 28 at 0:12
  • $\begingroup$ @Couchy My mistake, thanks for the correction! I've edited the answer to reflect that $\endgroup$
    – zacque
    Jul 28 at 0:12
1
$\begingroup$

I am in a little bit the same boat, in that I am (partly) self-taught and I will say that using a proof system has been a significant help to me (although I will say in conjunction with informal proofs, not instead of).

In my case the most approachable one has been Metamath (and offshoots of metamath, but none of those are as active or well developed as metamath itself). This is because metamath lets you see every step (in a more human-readable form than in a proof system where there is no particular focus on making reducing the number of steps or otherwise making them something you'd normally see at all).

Probably the biggest pitfall I have found is the learning curve (starting with just installing some of these systems, to the fact that the documentation for some of them assumes you already know type theory - which as far as I can tell is a problem of how they are explained as much as a genuine catch 22 in terms of whether you can really get started before you know what you are trying to learn). Oh, and choosing which system is most likely to be helpful in a crowded field - I installed quite a few before I got up the curve of learning how they work and figuring out what sorts of problems/exercises I might take on.

I could write more, including about my own journey from not having written a proof (formal or otherwise) in years, to being one of the significant contributors to the metamath proof collection, but perhaps the best place to point you is the mini-FAQ on https://us.metamath.org/index.html especially the question "Will Metamath help me learn abstract mathematics?"

$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

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