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

Fermat's Last Theorem – how it’s going

xenaproject.wordpress.com

Post reply on HN
Print view View original

11–20 of 216 posts

Re: Fermat's Last Theorem – how it’s going

#11

Post by hansvm »

coliveira wrote: post #6
seanwilson wrote: post #5

> This story really highlights, to me, the poor job which humans do of documenting modern mathematics. There appear to be so many things which are “known to the experts” but not correctly documented. The experts are in agreement that the important ideas are robust enough to withstand knocks like this, but the details of what is actually going on might not actually be where you expect them to be. For me, this is just…

> consider getting mathematics written down properly, i.e. in a formal system This was already tried, and failed (Hilbert). In the aftermath of the failure we learned that mathematics cannot be completely formalized. So this points to a fundamental problem with using AI to do math.

TFA isn't about AI; it's about taking the same arguments mathematicians are already writing down semi-formally with a hand-wavy argument that it could be made completely formal, and instead/also writing them down formally.

In cases where the Hilbert machine applies, the mathematician writing down the semi-formal argument already has to state the new axioms, justify them, and reason about how they apply, and the proposal would just take that "reason about how they apply" step and write it in a computer-verifiable way.

Re: Fermat's Last Theorem – how it’s going

#12

Post by ur-whale »

This article makes me very happy.

One of the many reasons I love math is the feeling I've always had that with it, we're building skyscraper-sized mental structures that are built on provably indestructible foundations.

With the advent of "modern" proofs, which involve large teams of Mathematicians who produce proof that are multiple hundreds of pages long and only understandable by a very, very tiny sliver of humanity (with the extreme case of Shinichi Mochizuki [1] where N=1), I honestly felt that math had lost its way.

Examples: graph coloring theorem, Fermat's last theorem, finite group classification theorem ... all of them with gigantic proofs, out of reach of most casual observers.

And lo and behold, someone found shaky stuff in a long proof, what a surprise.

But it looks like some Mathematicians feel the same way I do and have decided to do something about it by relying on the computers. Way to go guys !

[1] https://en.wikipedia.org/wiki/Shinichi_Mochizuki

Re: Fermat's Last Theorem – how it’s going

#13

Post by Etheryte »

bee_rider wrote: post #7

This hurts my engineer-brain. Just a reminder than the gap between us and mathematicians is about the same as the gap between us and everybody else (edit: in terms of math skills), just in the other direction, haha. Oh well, hopefully when they get the machines to solve math, they’ll still want them to run a couple percents faster every year.

[flagged]

Re: Fermat's Last Theorem – how it’s going

#14

Post by ur-whale »

coliveira wrote: post #6
seanwilson wrote: post #5

> This story really highlights, to me, the poor job which humans do of documenting modern mathematics. There appear to be so many things which are “known to the experts” but not correctly documented. The experts are in agreement that the important ideas are robust enough to withstand knocks like this, but the details of what is actually going on might not actually be where you expect them to be. For me, this is just…

> consider getting mathematics written down properly, i.e. in a formal system This was already tried, and failed (Hilbert). In the aftermath of the failure we learned that mathematics cannot be completely formalized. So this points to a fundamental problem with using AI to do math.

> This was already tried, and failed (Hilbert)

Who likely underestimated how hard it would be.

And who didn't have a 2024 computer on hand.

Re: Fermat's Last Theorem – how it’s going

#15

Post by ur-whale »

bee_rider wrote: post #7

This hurts my engineer-brain. Just a reminder than the gap between us and mathematicians is about the same as the gap between us and everybody else (edit: in terms of math skills), just in the other direction, haha. Oh well, hopefully when they get the machines to solve math, they’ll still want them to run a couple percents faster every year.

> about the same as the gap between us and everybody else

My bet: there is a very long list of skills for which the gap between you and a person randomly picked out the whole population is very large, and not in the direction you seem to think.

Re: Fermat's Last Theorem – how it’s going

#16

Post by dboreham »

munchler wrote: post #10
FredPret wrote: post #8

Earlier quoted context omitted.

Compilers have this very same habit!

Yes. In fact, Lean is a compiler and type checkers are theorem provers (by the Curry-Howard correspondence). Proofs are programs!

And Mathematics is Computer Science. Took me most of a lifetime to realize this.

Re: Fermat's Last Theorem – how it’s going

#20

Post by lambdaone »

coliveira wrote: post #6
seanwilson wrote: post #5

> This story really highlights, to me, the poor job which humans do of documenting modern mathematics. There appear to be so many things which are “known to the experts” but not correctly documented. The experts are in agreement that the important ideas are robust enough to withstand knocks like this, but the details of what is actually going on might not actually be where you expect them to be. For me, this is just…

> consider getting mathematics written down properly, i.e. in a formal system This was already tried, and failed (Hilbert). In the aftermath of the failure we learned that mathematics cannot be completely formalized. So this points to a fundamental problem with using AI to do math.

While it's true that mathematics cannot ever be completely formalized, per Gödel's incompleteness theorems, a huge amount of it obviously can, as is demonstrated by the fact that we can write it down in a reasonably rigorous way in a combination of conventional mathematical notation and plain English.

Nor is this in any way "a fundamental problem with using AI to do math".

Post reply on HN