The Fermat's Last Theorem Project(leanprover-community.github.io) |
The Fermat's Last Theorem Project(leanprover-community.github.io) |
I have ambivalent feelings about this project. On one hand, I think this is great, it approaches things in the right way, and I think the project has a big chance of being very successful.
On the other hand, the more successful mathematics in Lean becomes, the more entrenched a type-theoretic outlook on formalised mathematics will become. I think that is highly problematic as it makes the expression of theorems and theories more involved and complicated than it needs to be. This is not a stopping block, and people like Buzzard can just power through this. Also, that's just my opinion. I am trying to go with Practal a different path and prove this opinion to be true, but that will take time.
So I don't really understand the point made in this post. Dependent type theory makes the expression of some theorems more involved and complicated -- but set theory makes the expression of some other theorems more involved and complicated, simple type theory makes the expression of some others more involved etc etc. You're right that we're just powering through this: but formalising mathematics in Lean sometimes feels like fighting against type theory (and sometimes type theory is a very welcome foundation). The point really is that the Lean community, because of its viewpoint of "formalise all mathematics in one system", has been forced to figure out how to power through the areas where dependent type theory was not the ideal foundation. Maybe the same can be said of Mizar and set theory -- I'm unclear about how much formalisation in Mizar is motivated by "let's do this because it will be unproblematic in set theory" and how much is "let's choose to do battle with set theory". In mathlib we've decided to do everything so doing battle with dependent type theory is a necessary consequence. I find it hard to believe that another foundational choice (such as Practal) solves these sorts of problems: presumably what's actually true is that some stuff which is annoying in Lean is nice in Practal but some other stuff which is nice in Lean is annoying in Practal.
I think you understand the point perfectly well. You just don't believe that there can be a logical system better suited to a foundation of mathematics than first-order logic (set theory), simple type theory, or dependent type theory. You believe you will need to compromise, no matter which foundation you choose, so better just to pick your poison and get on with it. And I think pretty much everyone in the theorem proving space has that same opinion, so it is certainly a most reasonable opinion.
But I don't believe that the right logical foundation will make it harder to do mathematics on a computer than on paper, I think it will make it easier. In fact, I am pretty sure I have found that right logical foundation, Abstraction Logic [1]. I believe that it is indeed the best logical foundation, because it is simple and elegant (more so than any other foundation I am aware of), and it seems obvious that first-order logic, simple types, and dependent types are just special cases of it.
But a logic is not a working and proven system such as Lean + mathlib, so a lot of work needs to be done before my belief can be stated as a fact.
[1] https://lawrencecpaulson.github.io/2024/02/28/Gowers_bijecti...
[2] https://isarmathlib.org/func1.html#a_bij_def_alt
[3] https://mizar.uwb.edu.pl/forum/archive/2403/msg00001.html
I think the future looks like this: The resulting text will be natural language (LLM powered), layering upon the actual formal logic. I think Abstraction Logic is actually best suited for this scenario, and I am designing Practal from scratch for it.
What I am dismayed about is giving yet another area of computing to Microsoft. We all know that Microsoft ensures great care of the long term quality of software, right? Like when you click 'delete' on an email in outlook and have to wait 20 seconds for it to actually disappear.
Why not use coq instead?
I have no doubt that a similar project could be done in Coq. The fact that we're using Lean is a random historical coincidence. If we'd used Coq then you could ask "why not Lean".
Practal seems interesting and I scanned through the paper a year or two ago, but I have no reference point to evaluate it. I'm glad to see that you're still publishing about it.
How would you compare Practal with Lean, and what do you hope to prove (ha) with the project?
But the logic Practal is based on exists now. I am currently writing the basics of this logic up as a book [1]. Chapter 2 will be ready soon. I have learnt much about the logic in the last few months, also as a consequence of trying to implement it, and the book is based on this latest understanding. It all is really really simple, and I am trying to give it the proper form so that this becomes obvious.
I very much hope a first implementation is available this year, but this depends on how much I can work on it uninterrupted by money concerns.
In the end, what I am trying to prove with Practal is that formal logic doesn't make things more complicated. It actually makes things simpler.
Chapter 1 of the book is already available (you can buy it for £0), and Figure 2 vs. Figure 3 describes how type theory is different from Abstraction Logic, although I don't mention type theory explicitly at this point.
Future chapters take this view of the mathematical universe presented in chapter 1, and give it an algebraic and logical form.
Then I started to think about it and now I have the same question. When will a machine spit out a proof that we just can't understand? Just like how a dog will never understand the fundamental theorem of calculus, there are almost certainly ideas and concepts that we can't understand but the machines might.
My issue at the moment is with a line at the bottom of p.4, which effectively says that if k^n = xy for integers k, n, x, y, then k must be a multiple of y. Unless I'm missing something this is clearly false, for example 2^4 = 4 x 4.
But I don't know algebraic geometry, so I cannot say if there would be any advantage of doing it in Abstraction Logic compared to Lean. If you had any difficulties formalising algebraic geometry in Lean caused by static types (for example that there are no subtypes), then that might be where AL could help.
Also, could you do category theory in general in AL? Again, I don't know category theory well enough to say. But categories can certainly be represented as mathematical objects, so I don't see why not.
Do you have a minimal example in mind where you encountered problems in Lean?
(a + b − c)^n = (c − a)(c − b)g_1(n)
=> a + b − c = [(c − a)(c − b)g_1(n)]^(1/n)
=> g_1(n) | a + b - c
1) Whether it will still be science fiction by 2030;
2) Whether ITPs like Lean will be useful when working on this goal, or whether it will just be LLMs all the way.
But rather than asking questions like "will some system belch out a million line incomprehensible proof of the Riemann Hypothesis" one could ask the following much easier question. Computers are very helpful to mathematicians who do calculations right now, but are way way less helpful to mathematicians who prove theorems (there are many pure mathematicians in my department who have absolutely no use for computers in their research other than the obvious email/search/etc applications). Can we make tools which will help these mathematicians (who might be trying to prove theorems about uncountable and noncomputable objects) to do their day job? Again one can ask two questions:
1) Will this still be science fiction in 2030;
2) Will ITPs be involved?
And again I don't know the answers, but this work is an attempt by the Lean community to help ITPs understand precise statements of what's going on in modern number theory, in case that helps with (1).