Checking elementary proofs with proof checkers 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.
 A: 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:

*

*for weaker systems

*

*the proof in Metamath is 94 steps long,



*for stronger systems

*

*a couple dozen lines for the same proof in HOL Light,

*27 lines in Isabelle,

*30 lines in Mizar,

*16 statements stuffed into 9 lines in Coq

*comparably many lines in Lean's proof as for Coq, comparably as cryptic.




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

*

*Writing a Mizar Article in 9 Easy Steps (pdf)

*Mizar in a Nutshell (pdf)

*Getting to know the Mizar Mathematical Library
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.)
A: In addition to the excellent answer by Alex Nelson let me quote the proof that $\sqrt{2}$ is irrational written in the Naproche formal proof language:
Theorem. $\sqrt{2}$ is irrational.
Proof.
Assume that $\sqrt{2}$ is rational. Then there are integers $a$, $b$ such that $a^2=2b^2$ and $(a,b)=1$. Hence $a^2$ is even. Therefore $a$ is even. So there is an integer $c$ such that $a=2c$. Then $4c^2=2b^2$ and $2c^2=b^2$. So $b$ is even. Contradiction. Qed.
This is retyped from "The Naproche Project Controlled Natural Language Proof Checking of Mathematical Texts" paper, any typos are mine.
