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

31–40 of 42 posts

Re: The Fermat's Last Theorem Project

#31

Post by practal »

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…

Type theory vs. set theory is not the only choice. It is possible to combine their strengths in a new foundation: A single mathematical universe, just as in set theory, and higher-order features and abstraction, just as in type theory. Note that the listed strengths of each are the weaknesses of the other.

Re: The Fermat's Last Theorem Project

#32

Post by practal »

robinzfc wrote: post #28
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…

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…

That's a very good point. I have been strongly influenced by Isabelle and Isar, which get a lot of things right.

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.

Re: The Fermat's Last Theorem Project

#33

Post by kevinbuzzard »

practal wrote: post #27
kevinbuzzard wrote: post #18

Earlier quoted context omitted.

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…

I see! So I guess the proof of the pudding will be in the eating :-) Can you do algebraic geometry?

Re: The Fermat's Last Theorem Project

#34

Post by hughesjj »

n4r9 wrote: post #14
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.

If I'm not mistaken Fermat's last theroem isn't even featured in the proof. Like nowhere did I see a^n+b^n=c^n referenced in the proof,save for the end of page 1 and 3, but it's never featured in an equality. Just 'this implies this trust me bro'.

Re: The Fermat's Last Theorem Project

#35

Post by practal »

kevinbuzzard wrote: post #33
practal wrote: post #27

Earlier quoted context omitted.

> 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…

I see! So I guess the proof of the pudding will be in the eating :-) Can you do algebraic geometry?

If you can represent algebraic geometry through mathematical objects, operations and operators, then yes.

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?

Re: The Fermat's Last Theorem Project

#36

Post by n4r9 »

hughesjj wrote: post #34
n4r9 wrote: post #14

Earlier quoted context omitted.

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.

If I'm not mistaken Fermat's last theroem isn't even featured in the proof. Like nowhere did I see a^n+b^n=c^n referenced in the proof,save for the end of page 1 and 3, but it's never featured in an equality. Just 'this implies this trust me bro'.

I've actually had another quick look and I now have a vague idea of the outline. It's an attempted proof by contradiction, where a solution to FLT is applied to the binomial theorem and some arguments about integrality are made to form a contradiction.

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.

Re: The Fermat's Last Theorem Project

#37

Post by voldacar »

hughesjj wrote: post #17
voldacar wrote: post #12

Earlier quoted context omitted.

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'

My favorite part is "The derivative resembles the rhythm of a heartbeat."

Re: The Fermat's Last Theorem Project

#38

Post by pylua »

kevinbuzzard wrote: post #26
pylua wrote: post #25

Earlier quoted context omitted.

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…

2030 will be here before you know it. I am excited that this could help distribute knowledge of the field. Good luck and Godspeed!

Re: The Fermat's Last Theorem Project

#39

Post by JoeAltmaier »

pylua wrote: post #25
JoeAltmaier wrote: post #24

Earlier 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 ?

The original proof was the computer program, as I understand it.

Re: The Fermat's Last Theorem Project

#40

Post by downboots »

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

perhaps it was a veiled suggestion to use infinity in the proof (which would not fit in any margin) (?) https://en.wikipedia.org/wiki/Proof_by_infinite_descent
Post reply on HN