5
$\begingroup$

This is my first question in this part of StackExchange.

What I would like to achieve is the following.

Suppose I want to study ( or give a course on ) basic Real Analysis, I want to 1) document the axioms of Real Analysis, the theorems, and their proofs, in a tool ( I would call it a Proof IDE ) and 2) use the axioms and already documented theorems and their proofs to validate newly entered theorems/proofs.

( I have experience with many programming languages and mathematical software, especially Mathematica. I have done courses on Mathematical Logic and Computability. My research interests are mainly in Number Theory. )

My question is if there exists such a tool I am looking for? If not, where should I go to? Of course I am aware of the existence of Proof Assistants... but I would not where to start.

From what I have read in this question/answer What's the "Hello, World!" for proof assistants? there seems to be a huge gap in the language between theorems/proofs in mathematics textbooks and their "translation" in proof assistants. I would like the gap to be as small as possible.

$\endgroup$
3
  • $\begingroup$ I have tried out different proof assistants, and I find that those which have a dependent type theory as foundation are easiest to use. I believe that the difficulty is not as much about proof assistants. it is just a general phenomenon that doing things formally is much harder than doing them informally. $\endgroup$
    – Nico
    May 12, 2022 at 11:16
  • $\begingroup$ If you want to do classical mathematics, you can try lean. $\endgroup$
    – Nico
    May 12, 2022 at 11:17
  • $\begingroup$ I like the way the gap you refer to has been approached in Isabelle. I'm not posting an answer since I already described a bit of that in some answer and the following comments. There's also Larry Paulson's blog by way of introduction. It is also noteworthy that Isabelle/HOL is particularly strong in Analysis. $\endgroup$ May 17, 2022 at 12:55

1 Answer 1

3
$\begingroup$

As far as an entry point, I would highly recommend first trying the natural number game. It is fun (it is a game-based tutorial to Lean), it is short, it has a low barrier to entry (it is just in browser), and it would teach you things that are universal to most proof assistants (such as the inductive definition of the natural numbers and rewriting). Unfortunately, the sequel "real number game" hasn't been developed yet, since I think that is what you are looking for.

After that, I would find a proof assistant with:

  • Good documentation. You want to be able to learn the language well, so you want good documentation, especially a good tutorial.
  • Nice tooling. You want your experience working in that language to be positive with a good IDE, good interactivity, and good error messages.
  • A vibrant and welcoming community. When you get stuck (on something which is completely trivial mathematically), you want to be able to just ask for help in a low barrier environment. Many proof assistants have chat-based communities on Zulip and Discord.
  • Priorities similar to yours. Every proof assistant community comes with an implicit set of priorities. For example, do users tend to work on classical mathematics or constructive mathematics? Is the focus on building a library of mathematics, or on verifying algorithms in computer science, or on verifying computer code? Is it a single monolithic project with a central code repository, or is it a bunch of individual projects focusing on separate topics (which may or may not be compatible).

I think from what you said, Lean 3 might fit your interests. It has a decent tutorial (Theorem Proving in Lean), it uses a modern and popular IDE (VS Code), it has a very vibrant and supportive community on Zulip, and it is focused on building a library of classical mathematics covering all topics from undergraduate mathematics up to the cutting edge of research.

Its downsides are that Lean isn't very stable (especially with the current 2022 transition from Lean 3 to Lean 4). So unless your code goes into mathlib (the main mathematical repo), it will possibly bit rot. Also, mathlib already has a lot of analysis, but it is done in a very general way to make it widely applicable to other application. So for example, a theorem might be about Banach spaces instead of $\mathbb{R}^n$ for example.

A second option is Isabelle which is also focused on building a library of classical mathematics, and has a lot of analysis already. Also, maybe (???) its Isar style of proofs is more similar to what you are looking for with keeping proofs closer to the original mathematics, but honestly, I don't know if any proof assistant does this well since formal and informal mathematics are just so different.

But I don't want to say that these are the only options. See Proof assistants for beginners - a comparison for (opinionated) views on what proof assistants to start with. (Also, if you plan on doing very advanced mathematics, I would look at Are some proof assistants better suited for given areas of math than others? .) But don't let decision paralysis prevent you from learning one. Once you learn one, it is easier to transition to any other.

$\endgroup$
1
  • $\begingroup$ Thank you very much. Lean seems to be exactly what I need, for now anyway. Especially considering that Lean is well documented, active and alive. $\endgroup$ May 15, 2022 at 11:11

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge that you have read and understand our privacy policy and code of conduct.

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