General Questions

Stream: general

[Matthew Felgate]

Hi people. I'm new to Lean Therom Prover and have a few questions.

1. Has this software got the potential to prove all known mathematics?
2. Has the software ever proved a mathematical theorem to be incorrect?
3. Is there potential for Artificial Intelligence type software to hypothesize theorems and prove them correct or incorrect using this software to find new mathematical knowledge?
4. Is this software something a computer scientist with high-school level mathematics skills could contribute towards?
5. Is there a database of Theorems proven by this software?
6. Can a (new) theorem use other theorems as dependencies?
7. Are there mathematical theorems that can't be written in this software yet? How would the software be changed so they can?
8. What are the limits of this software?
9. Are there any beginner video guides on using this software? (on Youtube or learning platform such as Udemy etc)
10. Has the software been used to prove anything new? (previously unproven)
11. Are there some simple proofs that even a beginner could understand?

[Floris van Doorn]

Let me take a stab at some of the questions.

[Johan Commelin]

1. Yes. In theory certainly. In practice, you need lots of people, lots of time, etc...
2. If you are very strict, yes. But usually, a little change in the assumption fixes the theorem. (Someone forgot to exclude the empty set, etc...) But see https://www.math.sciences.univ-nantes.fr/~gouezel/articles/morse_lemma.pdf
3. Hard question. So far this hasn't gotten beyond trivialities.
4. Depends. At the moment there is still a lot of low-hanging fruit. And you can certainly help with the algorithmic part.
5. What is a database? There is a bunch of source files containing the definitions, theorems and proofs. See mathlib.
6. Short answer: No. Long answer: People are trying to do this, but it is complicated.
7. The problem is usually that you can't even state the theorem, because you first need 1500 definition in place. And those aren't there yet. But see 1. In theory this isn't a problem.
8. I'll skip this one. It's very broad.

[Floris van Doorn]

(1) Yes, all main proof assistants, including Lean, can prove all known mathematics in principle. The main difference between the systems is how convenient it is to do this. The goal of Lean is to be more (or at least as) convenient as other proof assistants.

[Johan Commelin]

9. Yes, search Youtube. Although I haven't watched them yet.
10. Not really.
11. Certainly. You could look up the definition of the complex numbers, for example. After that come a bunch of proofs of basic properties.

[Floris van Doorn]

Ah, Johan had already started typing an answer. Let me skip some of his...

[Patrick Massot]

Either I don't understand question 7 or I don't understand Johan's answer

[Bryan Gin-ge Chen]

This recent thread has a bunch of links to resources for beginners, including, some videos on youtube (which I haven't watched). Most people, as I understand it, first figure out how to install Lean on their computer (following the links here https://github.com/leanprover-community/mathlib#installation) then work their way through the book "Theorem Proving in Lean". I personally also found the book "Logic and Proof" helpful.

[Miguel Raz Guzmán Macedo]

Hey all!
Great forum and appreciate all the answers.
@Patrick Massot sorry if I'm repeating myself, but do you have a link on the software you used to create websites with clickable proofs that unfold Lean proofs?

[Johan Commelin]

Re 7. Some theorems currently can't be written yet. The reason is that we don't have the "nouns" and "verbs" to do so. We first need loads of definitions, before we can "write" the theorem.

[Patrick Massot]

@Miguel Raz Guzmán Macedo Sorry I missed your question. The answer is: https://github.com/leanprover-community/format_lean

[Floris van Doorn]

(4): Yes, definitely. There are computer scientists working on Lean. There is plenty of progress that can just be made on writing tactics / decision procedures. And there is still some first-year undergraduate math missing (mostly calculus), which is probably feasible.
(5): Mathlib is the math library for Lean, and has many proven theorems: Here is the link: https://github.com/leanprover-community/mathlib

[Patrick Massot]

Oops, Johan I meant 6

[Floris van Doorn]

(6): Yes, theorems can use other theorems in their proofs. Almost all proofs do this.
Johan probably answered the question whether proof assistants can use the proofs of different proof assistants (e.g. can Lean use Coq's proofs). This is very hard in general, but there have been some accomplishments in this area.

[Floris van Doorn]

(11): I recommend http://neil-strickland.staff.shef.ac.uk/dagstuhl/ which has a couple of formalized proofs with a detailed explanation (see the links under Formalisations). Especially the Primes example is good.

[Patrick Massot]

About question 4 (contributing): it very much depend what you want to contribute to. Working on Lean itself is a very difficult very specialized task. Only a handful of people in the world do that, under close supervision by Leo de Moura. However almost anyone with basic math knowledge can contribute to Lean's maths library mathlib, or contribute to documention.

[Johan Commelin]

Oops, Johan I meant 6

@Patrick Massot Aaah, my answer is nonsense. I read to fast. I thought the question was about theorem provers using each others results. Should have read better.

[Johan Commelin]

(deleted)

[Floris van Doorn]

(10) It depends on whether you mean Lean specifically or also other software, and what mathematical results you count. Let me give two examples:

• In the area of homotopy type theory - a relatively new field connecting to both logic and geometry (algebraic topology) - many results have been formalized, and some results had been formalized before being carefully written up on paper. Lean 2 (an older version of Lean) had a homotopy type theory library: https://github.com/leanprover/lean2/blob/master/hott/hott.md
• Tom Hales proved an open problem called the Kepler conjecture in mathematics. It took many years for mathematicians to review this proof, so he formally verified it in the proof assistant HOL Light (the paper proof was published before the formal proof was completed though).

[Floris van Doorn]

More on (10): since the main goal of proof assistants is to check proofs given by the user, the user basically has to already know the proof before they can formalize it. There is another branch of formal proof called Automated Theorem Proving where the software finds mathematical proofs. They have more success in proving new results.

[Matthew Felgate]

Thanks for all the answers. Genuinely appreciated.

[Mason McBride]

If I use a tactic without specifying any parameters and leans matches the pattern for me, is there a way I can make lean tell me what paramters it passed? For example if I just said "add_sub," but I want to know the "a b c" it uses.

[Yaël Dillies]

you can wrap the tactic call in show_term as in show_term { rw add_sub }

[Mason McBride]

Thank you for your kindness!

[Yaël Dillies]

You can mostly thank my university work to keep me up that late :upside_down: