I think this is awesome. I do wonder if projects like this will are the first step for humans to completely hand over proving to machines.
The Fermat's Last Theorem Project
21–30 of 42 posts
Re: The Fermat's Last Theorem Project
#22Very smart to open up the project from the start to make collaboration possible. 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…
Could you elaborate on what alternative to a 'type-theoretic outlook' you're thinking of? Pure set theory? Something without types at all, somehow? I don't know enough about the space to understand how type theory would make things "more complicated" as opposed to just being a helpful tool
Re: The Fermat's Last Theorem Project
#23I think this is awesome. I do wonder if projects like this will are the first step for humans to completely hand over proving to machines.
At first I was going to react to you using "completely" because I thought the obvious thing was that the machines would remain a tool and maybe become collaborators.
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.
Re: The Fermat's Last Theorem Project
#24I think this is awesome. I do wonder if projects like this will are the first step for humans to completely hand over proving to machines.
At first I was going to react to you using "completely" because I thought the obvious thing was that the machines would remain a tool and maybe become collaborators. 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 con…
Already happened? The four-color map theorem was a computer program exhaustively going through some solution-space until it found one. Thousands of lines of logic spit out on paper. Probably impossible for any human to comprehend.
Re: The Fermat's Last Theorem Project
#25Earlier quoted context omitted.
At first I was going to react to you using "completely" because I thought the obvious thing was that the machines would remain a tool and maybe become collaborators. 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 con…
Already happened? The four-color map theorem was a computer program exhaustively going through some solution-space until it found one. Thousands of lines of logic spit out on paper. Probably impossible for any human to comprehend.
That had been proven previously ? I guess so has flt, but it will eventually solve an unsolved problem ?
Re: The Fermat's Last Theorem Project
#26Earlier quoted context omitted.
Already happened? The four-color map theorem was a computer program exhaustively going through some solution-space until it found one. Thousands of lines of logic spit out on paper. Probably impossible for any human to comprehend.
That had been proven previously ? I guess so has flt, but it will eventually solve an unsolved problem ?
Right now, machines proving stuff which is interesting to lots of human mathematicians but unprovable by them is science fiction. People seem to have very different opinions on the following two questions:
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).
Re: The Fermat's Last Theorem Project
#27Very smart to open up the project from the start to make collaboration possible. 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…
My impression is that some parts of maths work best using set theory, some parts work best using type theory, some work best using a category-theoretic foundation and ignoring size issues etc etc. There's no one "best" foundations, and mathematicians on paper just freely (and mostly unknowingly) switch between foundations depending on what they're doing. This is problematic for a project such as formalising FLT becau…
> So I don't really understand the point made in this post.
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.
Re: The Fermat's Last Theorem Project
#28Very smart to open up the project from the start to make collaboration possible. 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…
Another aspect of this is the readability of the resulting text. The role of a proof in mathematics is not only to certify that an assertion is true, but also to communicate to mathematicians why it is true. Lean and Coq verification scripts are not readable in this sense. They do certify that assertions of theorems are true and (at the current state of technology) that the author of the script most likely knows why they are true, but it is close to impossible for a reader to see what is going on in the proof without running the script step by step in software. The Mizar proof language and Isabelle/Isar were designed to communicate as well and proofs written in those languages can be read and understood directly by humans. For a comparison how the same proof of a simple theorem looks like in Lean, Isabelle/HOL, Isabelle/ZF and Mizar see [1], [2] and [3].
[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
Re: The Fermat's Last Theorem Project
#29Very smart to open up the project from the start to make collaboration possible. 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 have no experience in this area, but when I last looked Lean and mm0 were the interesting theorem proving systems to me. Lean for its momentum and big projects, and mm0 for its goal of producing a minimal kernel proven down to machine code. 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.…
Well, the most important difference is that Lean exists and is going strong, and Practal doesn't even exist yet.
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.
Re: The Fermat's Last Theorem Project
#30Very smart to open up the project from the start to make collaboration possible. 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…
Could you elaborate on what alternative to a 'type-theoretic outlook' you're thinking of? Pure set theory? Something without types at all, somehow? I don't know enough about the space to understand how type theory would make things "more complicated" as opposed to just being a helpful tool
I am writing about this here: http://abstractionlogic.com
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.