Zulip Chat Archive

Stream: general

Topic: General Questions


Matthew Felgate (Oct 11 2019 at 16:48):

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 (Oct 11 2019 at 17:03):

Let me take a stab at some of the questions.

Johan Commelin (Oct 11 2019 at 17:04):

  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 (Oct 11 2019 at 17:04):

(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 (Oct 11 2019 at 17:06):

  1. Yes, search Youtube. Although I haven't watched them yet.
  2. Not really.
  3. 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 (Oct 11 2019 at 17:07):

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

Patrick Massot (Oct 11 2019 at 17:07):

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

Bryan Gin-ge Chen (Oct 11 2019 at 17:07):

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 (Oct 11 2019 at 17:08):

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 (Oct 11 2019 at 17:08):

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 (Oct 11 2019 at 17:09):

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

Floris van Doorn (Oct 11 2019 at 17:09):

(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 (Oct 11 2019 at 17:09):

Oops, Johan I meant 6

Floris van Doorn (Oct 11 2019 at 17:11):

(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 (Oct 11 2019 at 17:12):

(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 (Oct 11 2019 at 17:12):

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 (Oct 11 2019 at 17:14):

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 (Oct 11 2019 at 17:16):

(deleted)

Floris van Doorn (Oct 11 2019 at 17:39):

(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 (Oct 11 2019 at 17:41):

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 (Oct 11 2019 at 19:14):

Thanks for all the answers. Genuinely appreciated.

Mason McBride (Feb 16 2022 at 02:31):

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 (Feb 16 2022 at 02:33):

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

Mason McBride (Feb 16 2022 at 02:43):

Thank you for your kindness!

Yaël Dillies (Feb 16 2022 at 02:49):

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


Last updated: Dec 20 2023 at 11:08 UTC