Hacker News Board Hacker News, browsed like a classic message board
Live data from Hacker News

The Fermat's Last Theorem Project

leanprover-community.github.io

Post reply on HN
Print view View original

11–20 of 42 posts

Re: The Fermat's Last Theorem Project

#11

Post by practal »

Very 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 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.

Re: The Fermat's Last Theorem Project

#13

Post by cjfd »

practal wrote: post #11

Very 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 think the type-theoretic outlook on formalized mathematics is actually great, much nicer than set theory anyway. Set theory is a bit like an untyped programming language. You get to ask 'interesting' questions like whether the trivial group is equal to the number 5 which makes sense because both of them are actually a set.

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?

Re: The Fermat's Last Theorem Project

#14

Post by n4r9 »

levn11 wrote: post #2

https://www.techrxiv.org/users/717330/articles/702287-on-fer...

This would definitely benefit from a bit more explanatory text as I'm struggling to understand what you've shown. The crux seems to be that if a^n+b^n=c^n then (c-a)(c-b) divides (a+b-c)^n. I haven't been through all the details of this, but I also don't see how that implies FLT.

Re: The Fermat's Last Theorem Project

#15

Post by infogulch »

practal wrote: post #11

Very 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.

How would you compare Practal with Lean, and what do you hope to prove (ha) with the project?

Re: The Fermat's Last Theorem Project

#16

Post by msfanboy-aahum »

cjfd wrote: post #13
practal wrote: post #11

Very 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 think the type-theoretic outlook on formalized mathematics is actually great, much nicer than set theory anyway. Set theory is a bit like an untyped programming language. You get to ask 'interesting' questions like whether the trivial group is equal to the number 5 which makes sense because both of them are actually a set. What I am dismayed about is giving yet another area of computing to Microsoft. We all know th…

The main dev of Lean no longer works at MS. So currently there are basically no ties to MS. Lean is developed by the Lean FRO, which aims at being selfsustainable in ~4 yrs from now.

Re: The Fermat's Last Theorem Project

#17

Post by hughesjj »

voldacar wrote: post #12
levn11 wrote: post #6

Earlier quoted context omitted.

which part

The part in which FLT is derived from the binomial theorem, lol.

Nah not derived, set equal to from the outset with essentially no explanatory test throughout but with enough effort to insert some arbitrary graphs and label them with 'hey neato look at the vibes'

Re: The Fermat's Last Theorem Project

#18

Post by kevinbuzzard »

practal wrote: post #11

Very 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 because it involves developing mathematics in a bunch of different areas (algebra, analysis, geometry) where different foundations might be more appropriate (for example getting homological algebra working in dependent type theory has been annoying and hard for all the wrong reasons, and it's taken the Lean community years to figure out how to do it).

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.

Re: The Fermat's Last Theorem Project

#19

Post by kevinbuzzard »

cjfd wrote: post #13
practal wrote: post #11

Very 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 think the type-theoretic outlook on formalized mathematics is actually great, much nicer than set theory anyway. Set theory is a bit like an untyped programming language. You get to ask 'interesting' questions like whether the trivial group is equal to the number 5 which makes sense because both of them are actually a set. What I am dismayed about is giving yet another area of computing to Microsoft. We all know th…

Lean is free and open source and nothing to do with MS. Check out https://lean-lang.org/ and https://github.com/leanprover/lean4 -- no mention of MS or MSR (where de Moura was where he developed Lean 3 and started on Lean 4).

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".

Re: The Fermat's Last Theorem Project

#20

Post by kevinbuzzard »

mehulashah wrote: post #7

I wonder if after all that work, we might automatically reduce the proof and discover a simpler one that could have been included in the “margin”.

I highly doubt that the proof will get small enough to fit into a margin, but history shows that it's not at all unreasonable to expect simplifications/generalisations of the argument to come out of a formalisation (for example this happened with the Liquid Tensor Experiment, where dependence on stable homotopy groups of sphere was completely removed from the argument). I think it is unreasonable to expect that at the end of an FLT formalisation there will be no mention of elliptic curves, modular forms, Galois representations etc (the standard tools used by Wiles to prove the result in the 90s and which have themselves been simplified and generalised by mathematicians such as Taylor and Kisin since then). And you'll need quite a big margin to get all that stuff in.
Post reply on HN