Very Basic Question

Stream: new members

[Noah Fields]

Hello to all. I'm a first semester graduate student in applied computer science with an interest in theory. I just made an account after playing some of the Natural Numbers Game. I just want to make sure I understand the most basic ideas.

Lean is a theorem prover where you give it facts and theorems and prove new facts and theorems. As such, one could do things such as:

• Work through the entirety of Russell and Whitehead's Principia Mathematica
• Build up the concept of complexity classes and try to use Lean to solve P = NP
• Demonstrate Godel's Incompleteness Theorem by encoding mathematical statements with unique numbers like he did
• Create abstract group theoretic objects as the Natural Numbers game FAQ mentions has been done

All built from basic theoretical principles like the Peano axioms.

And, if I were to keep going through various practice problems to learn how to use Lean and sharpen my abstract mathematical knowledge, I could (with a lot of practice) potentially reach the point where I am working with unsolved problems in Lean and make new mathematical discoveries. This, of course, is not something accomplished in an afternoon, but it would be possible.

Is this an accurate summary of what Lean is capable of and what I, as a nascent computer scientist, could do with it?

[Kevin Buzzard]

Yeah kind of, although I think Russell and Whitehead were working in a different foundational system to Lean's (indeed it only takes three characters to prove 1+1=2 in Lean rather than 100+ pages). Right now you can in theory use Lean to solve P=NP but all that would happen woudl be that you're making it more difficult for yourself, because doing mathematics on paper is easier than doing it in Lean. Lean can help with easy stuff, but easy stuff is easy. Lean doesn't do mathematics automatically yet, it just checks your inputs are valid mathematics.

[Noah Fields]

Kevin Buzzard said:

Yeah kind of, although I think Russell and Whitehead were working in a different foundational system to Lean's (indeed it only takes three characters to prove 1+1=2 in Lean rather than 100+ pages). Right now you can in theory use Lean to solve P=NP but all that would happen woudl be that you're making it more difficult for yourself, because doing mathematics on paper is easier than doing it in Lean. Lean can help with easy stuff, but easy stuff is easy. Lean doesn't do mathematics automatically yet, it just checks your inputs are valid mathematics.

Aww. I kind of wanted to make a "Natural Numbers Game: Principia Edition" that walked someone through the Principia Mathematica. That is, ultimately, kind of what the Natural Numbers game is - building mathematical properties from the ground up, but starting from Peano's axioms instead (and saving a heck of a lot of time in the process). I suspect it would not be impossible to give Lean the Principia's axioms and use only those, albeit with "But why would you want to?" hanging over things.

Regarding "Lean can help with easy stuff, but easy stuff is easy - " If it did in fact help mathematicians find new abstract group theoretic objects, then it can help prove hard stuff too, though it doesn't make those things not hard anymore - it's just another tool in the toolbox that can help with some tasks, like a calculator. My understanding is that the main benefit of such a system as Lean is that it reduces the risk of a mistake - since the computer can verify that A really does lead to B, any case of incorrect logic [ex: Using a + b = b + a if that is not proven for whatever types a and b are] will be found and highlighted by the system, even if they are subtle enough that a human on pencil & paper might miss them. Anecdotally, I don't think I could have beaten the Natural Numbers Game by hand half as easily, which suggests that it works.

Obviously, if Lean made P = NP trivial, someone would have done it. I used it as an example of both how abstract things can get, since the definition of a complexity class requires much more advanced concepts than natural numbers, and how it could (in theory) be used to tackle very difficult problems. It sounds like my intuition is right and it indeed can. I didn't mean to suggest that I thought Lean was a miracle machine that you could just throw the Millennium Problems at and it would magic the answers to you, but if someone sufficiently dedicated could code in Lean concepts like Turing machines and polynomial time reductions, and then use it as an assistant for proving NP-Completeness of a problem or trying out a P = NP proof or disproof, that certainly seems like a powerful tool.

My computer science learning has equipped me to make the following claim: Lean doing mathematics automatically is not possible in the general case. If Lean were given a hypothesis and said "Prove or disprove this", this is the halting problem and is Turing-undecidable. That is not to say it would not be successful on some, or even most, inputs, and certainly not that it is pointless to make Lean do automatic mathematics for those particular cases, but it is mathematically guaranteed that the program would, for some hypotheses, run for an infinite length of time and never arrive at an answer, or (more likely) time out or use the machine's full resources and crash. It does not matter how carefully such an automatic solver is written. It is literally mathematically impossible to make it solve all cases.

[Patrick Johnson]

Using Lean as a tool (assistant) for manual theorem proving and using Lean as an automated prover are two very different things. The impression you got from NNG doesn't accurately reflect how solving advanced math problems look like. In NNG, you just "follow your nose", try induction or cases or whatever "feels" right and it works because it's "crafted" to work.

In real math there are advanced problems for which you need an idea. You then try to elaborate the idea and verify each step rigorously. At the end, you formalize the proof in Lean. But Lean can't help you get an idea. Regarding P=NP, the problem is that nobody has an idea how to even approach that problem. Lean can't really help about that. I don't think there are any mathematical objects or ideas that are formalized in Lean but not used in real math (except maybe filters, but they are the artifact of DTT's technical limitations to represent what mathematicians can abstract intuitively). There are many proofs that are proved on paper, but not formalized in Lean, simply because formalization is much slower than proof on paper. For example, Fermat's last theorem is proved almost 30 years ago, but the proof is so complex that I dare to say it won't be formalized in the next 20 years. Another example is Perelman's proof of the Poincaré conjecture.

Regarding automated theorem proving, the most successful approach so far was using SAT solvers. For example, Marijn Heule proved many theorems by reducing them to a CNF formula and solving using an advanced SAT solver. However, not all problems can be easily reduced to a CNF. Using AI to automatically prove theorems in Lean is, in my opinion, very distant future. There are AIs that can prove some trivial theorems in Lean, but anything more complex is far from reach. Proving advanced theorems (in reasonable time) requires a very general AI, because many problems from real life can be modeled in math, thus if we develop an AI to prove any theorem faster than humans, we already have general artificial intelligence which can beat humans in any other task. That is not going to happen soon, in my opinion.

[Patrick Massot]

Patrick Johnson said:

I don't think there are any mathematical objects or ideas that are formalized in Lean but not used in real math (except maybe filters, but they are the artifact of DTT's technical limitations to represent what mathematicians can abstract intuitively).

That comment about filters is simply wrong. Using filters instead of bluff or stuttering has nothing to do with foundations.

[Kevin Buzzard]

Right -- filters are a beautiful abstraction which are used precisely because they unify many concepts

[Noah Fields]

It sounds like I was both right and wrong. In my head, I was imagining that with sufficient time and practice, any theorem became like the Natural Numbers game - obviously much, much, much harder since the NNG was literally meant as a Lean tutorial, but it would still be a matter of "I know A; I want to prove B; here are all the things I know and have proven; how can I get there?" And then, if you're really good at math and/or Lean, you can do that even for cases where B has never been proven by anyone before, and then you get a cool paper out of it. It sounds like that isn't wrong (if it was wrong it would go against a lot of my math knowledge, actually, not just what I learned here), but Lean is less a tool to get there, and more a tool to make sure your already existing work was correct.

It does raise the terrifying question that a commonly touted theorem might actually be wrong. What if it turns out Perelman's Poincare conjecture proof cannot be verified in Lean because it's wrong? I guess since he turned down the prize they wouldn't have to ask for their money back. Regardless, I understand that this is a big reason Lean and similar systems exist (the idea was brought up in a course I took, that these systems exist to make sure the mathematics we use are as sound as possible). Overall, Lean is perhaps a different tool than I thought it was when I made my first message, but nevertheless seems very cool and a tool I will want to understand.

Regarding SAT solvers: My research involves SMT solvers so I'm right ahead of you on that one! :D I'm a bit surprised that Marijn proved theorems by reducing them to CNF-SAT, rather than a more sophisticated SMT form. It's possible to encode advanced mathematical concepts in SAT, but a lot harder, and SMT solvers enable things like encoding numbers in the expression directly (which might help prove things like inequalities). Was SAT really the easiest way forward for those problems?

[Patrick Johnson]

Noah Fields said:

Regarding SAT solvers: My research involves SMT solvers so I'm right ahead of you on that one! :D I'm a bit surprised that Marijn proved theorems by reducing them to CNF-SAT, rather than a more sophisticated SMT form. It's possible to encode advanced mathematical concepts in SAT, but a lot harder, and SMT solvers enable things like encoding numbers in the expression directly (which might help prove things like inequalities). Was SAT really the easiest way forward for those problems?

Here is a chart presented by Nikolaj Björner.
SMT solvers are more expressive, but SAT solvers are far more efficient.