3
$\begingroup$

I am not sure if this is the right place to post this, but I have seen discussions related to proof checking here, so let me post it. If there is better place for it, please give me a hint as to where I might put this, and I will move it (hopefully I can do that easily).

I am interested in finding the most effective proof assistant, if it exists, to check the correctness of elementary proofs in number theory (I will give an example of what I have in mind ahead). Whatever system is recommended, it needs to be able to deal with the elementary arithmetic of reals and integers. First order logic and universal second order quantifiers over (infinite) sets of integers suffice. If inductive proofs can be checked, that will be a plus, but I am happy to start without such a capability.

As an example of the kinds of propositions of which proofs I would like to check, consider the irrationality of the square root of 2 and the standard proof of this by contradiction, to wit:

Suppose $c$ is rational (where $c=\sqrt 2$). Then there exist positive integers $a, b$, which are relatively prime (this can be written in FOL … ) such that $c=a/b$. But then, $2=c^2=a^2/b^2 \Rightarrow$ there exists a positive integer $k$ such that $a=2k$. But $a=2k \Rightarrow \ldots \Rightarrow b^2=2k^2$, so there is also a positive integer $k$ such that $b=2k$. This contradicts a and b being relatively prime, end of proof.

Surely, one has to do this quite very carefully according to how the system is supposed to be used, but hopefully you get the jist of it.

Now, what I want is something that will work best for THESE kinds of proofs without a problem (if it exists) and also - IF POSSIBLE - something that is relatively easy and straightforward to use and does not have a steep learning curve in order to get started. NOTE: I want to check proofs that have already been produced by hand, not try to find them.

It is my hope that the system be something that is freely and easily accessible, and which will work on a standard Windows (or Mac, or Linux) based laptop with not a huge amount of RAM or storage. Speed is not an issue, as long as one can get, say, a 5 page hand crafted proof (obviously more after it has been written into the system) checked in a reasonable amount of time (say, a working day).

I am aware of the existence of systems like Lean (which version?), etc., but I have never used any of these systems, so I do not really know what is best here. Now is the time for me to start, with the hope that I will bring this to class some day and have (college) students try their hand with a very nice selection of theorems with elementary proofs.

I thank you in advance for your help and advice.

$\endgroup$
5
  • 3
    $\begingroup$ There will shortly (as in a week or two) be a proof-asssistant stack exchange site area51.stackexchange.com/proposals/126242/proof-assistants I was going to say you should certainly post your question there if you don't get a good response here, but then I realized that questions like "What is the best proof assistant for X" might be too acrimonious for a site designed to bring together devotees of multiple different proof assistants. Still I don't think there is a rule against such questions yet. $\endgroup$
    – Will Sawin
    Nov 29, 2021 at 20:25
  • 1
    $\begingroup$ With regards to your actual question, if the goal is to get college students to input elementary proofs into the system, this is something people like Kevin Buzzard have actually done in Lean (3), and if you take that route you can go to the Zulip chat for advice from people who have done similar things. $\endgroup$
    – Will Sawin
    Nov 29, 2021 at 20:27
  • $\begingroup$ @WillSawin Great, thank you for both comments and your suggestions! I will definitively post it there. Hopefully in the meantime someone can suggest something? $\endgroup$
    – EGME
    Nov 30, 2021 at 7:06
  • 5
    $\begingroup$ cs.ru.nl/~freek/100 has pointers to proofs of the irrationality of $\sqrt 2$ in a number of systems, so you could have a look and see which feels most natural to you. $\endgroup$ Nov 30, 2021 at 7:29
  • 1
    $\begingroup$ For those interested in Proof Assistants, there is a new proposed SE site ProofAssistants $\endgroup$
    – Guy Coder
    Dec 2, 2021 at 20:25

1 Answer 1

3
$\begingroup$

I can suggest some systems that I know, but I don't think there's exactly a solution which you are looking for.

Now, what I want is something that will work best for THESE kinds of proofs without a problem (if it exists) and also - IF POSSIBLE - something that is relatively easy and straightforward to use and does not have a steep learning curve in order to get started. NOTE: I want to check proofs that have already been produced by hand, not try to find them.

How formal are you willing to make the proofs? This is the biggest constraint. As the proofs have "bigger steps" in reasoning (even resembling pedantic proofs found in undergraduate level courses), you need a more powerful checker.

But as the proofs become more insanely pedantic, showing steps which humans take for granted, you can use "weaker" and more Spartan provers. For example, the proof $\sqrt{2}\notin\mathbb{Q}$ in different systems:

It is my hope that the system be something that is freely and easily accessible, and which will work on a standard Windows (or Mac, or Linux) based laptop with not a huge amount of RAM or storage. Speed is not an issue, as long as one can get, say, a 5 page hand crafted proof (obviously more after it has been written into the system) checked in a reasonable amount of time (say, a working day).

I'm not sure what this means these days. Like, is this a Raspberry Pi 2? Or a "generic laptop" with a ~2 GHz processor, a few gigs of RAM, and around 100 GB hard disk?

In the first case, the biggest constraint may be the amount of RAM.

Most proof checkers are quick; the time consuming part will be writing up the formalization of the proof, and trying to debug why a formalization is inadequate.


Let me now review the theorem provers I know about, from least resource intensive to most demanding.

Metamath

Metamath is a lean, mean, proof-checking machine.

Advantages

  • Very Spartan, requires minimal hardware
  • Fast
  • I think there's Friendly community (I have emailed Norm Megill directly, and he's friendly and helpful; there's also a Google Groups for Metamath, though I haven't interacted with it)
  • Very pedantic proofs
  • Decent library

Disadvantages

  • Very Spartan, so you may need to prove a lot more "infrastructure lemmas" than you'd like
  • Can be cryptic (doesn't resemble ordinary mathematical proofs)
  • Steep learning curve (at least, for me)
  • Very pedantic proofs: what's obvious to me is not obvious to Metamath.

Resources

There's a google groups page for Metamath, and the main page has a recommended learning path. I'd be interested in any other resources or tutorials, personally, but I do not know any.

See also: For a comparably minimal system with type theoretic foundations, see Nick de Bruijn's Automath, the book Selected Papers on Automath, and Wiedijk's implementation.

Mizar

Given the hardware constraints, you might want to consider Mizar.

Advantages:

  • Resembles working mathematics
  • Large library
  • Good performance
  • Foundations are Set Theory and Logic
  • Friendly community, with a Mizar user service

Disadvantages:

  • Cryptic feedback from the system.
  • Can be difficult to navigate the library.
  • Can have steep learning curve.

References

HOL Light

If you know OCaml, then HOL Light may be a possibility.

It's an LCF-style prover, where the user communicates to the prover via "tactics" instructions. This makes a proof cryptic but guarantees theorems are proven. It can be made human-readable ("declarative proof style") using Mizar mode.

Advantages:

  • Lean on resources
  • Very small kernel (so small likelihood of bugs)
  • Programmable
  • Friendly community

Disadvantages:

  • Higher order logic is kinda strange as a foundation of mathematics
  • Cryptic tactic language
  • Can be difficult if you don't know OCaml
  • Smaller library

References:

I actually don't know any good references not on the linked website.

Coq

Similar to HOL Light, except with different foundations (using Type Theory instead of Higher Order Logic)...actually, early documentation described Coq as "LCF + Automath".

If you don't know type theory as a foundation of mathematics, then this is probably going to be difficult to learn. I would suggest learning Automath first (reading the first few chapters of Selected Papers on Automath, alongside Freek Wiedijk's formalization of foundations in Automath, is a great way to learn it).

Advantages

  • Big friendly community
  • Decent library
  • Powerful prover

Disadvantages

  • Can require a lot of RAM at times, like 32 GB big
  • Long learning curve, if you don't know CiC foundations
  • Cryptic proof language, without a declarative style proof option
  • Does not resemble ordinary mathematics
  • Can be confusing to navigate the library

Resources

I learned how to use CoqIDE from this video from Andrej Bauer.

See also a short intro to Coq and Software Foundations in Coq.

(Lean is similar to Coq, but I don't know it well enough to comment on it. Despite its name, Lean is rather resource intensive.)

$\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.