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

121–130 of 216 posts

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

#121

Post by smj-edison »

XorNot wrote: post #106
adrian_b wrote: post #101

Earlier quoted context omitted.

Using vague terms like "obvious" or "standard techniques" is doubtless wrong, but I would not see any problem in a paper basing its conclusions on demonstrations from a source listed in the bibliography, except that in many cases those who read the paper are unable to obtain access to the works from the bibliography. Even worse is when the bibliography contains abbreviated references, from which it is impossible to d…

This is a wider problem in general and an odd bit of history: scientific papers pre-date the internet, and as such the reference system exists pre-computation. the DX-DOI system is a substantial improvement, but it's not the convention or expectation - and IMO also insufficient. Realistically, all papers should just be including a list of hashes which can be resolved exactly back to the reference material, with the c…

The issue with hashing is that it's really tricky to do that with mixed media. Do you hash the text? The figures? What if it's a PDF scan of a different resolution? I think it's a cool idea—but you'd have to figure out how to handle other media, metadata, revisions, etc, etc.

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

#122

Post by eab- »

rstuart4133 wrote: post #93
impendia wrote: post #48

Earlier quoted context omitted.

Speaking as a current researcher in pure math -- you're right, but I don't think this is easily resolved. Math research papers are written for other specialists in the field. Sometimes too few details are provided; indeed I commonly gripe about this when asked to do peer review; but to truly provide all the details would make papers far, far longer. Here is an elementary example, which could be worked out by anyone w…

> I don't think this is easily resolved. It is technically resolvable. Just insist on Lean (or some other formal verifier) proofs for everything. It looks to me like math is heading that way, but a lot of mathematicians will have to die before its the accepted practice. Mathematicians who are already doing formal proofs are discovering it have the same properties as shared computer code. Those properties have have le…

> Just insist on Lean (or some other formal verifier) proofs for everything

Lean is too inflexible for this, in my opinion. Maybe I'm not dreaming big enough, but I think there'll have to be one more big idea to make this possible; I think the typeclass inference systems we use these days are a severe bottleneck, for one, and I think it's very, very tedious to state some things in Lean (my go-to example is the finite-dimensionality of modular forms of level 1 - the contour integral is a bitch and has a lot of technicalities)

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

#123

Post by CJefferson »

mostly_a_lurker wrote: post #49
bell-cot wrote: post #41

Earlier quoted context omitted.

> The crowd went wild; I've never made a group of experts so angry as... Also not a number theorist...but I'd bet those so-called experts had invested far, far too many of their man-years in that unproven conjecture. All of which effort and edifice would collapse into the dumpster if some snot-nosed little upstart like you, using crude computation , achieved overnight fame by finding a counter-example. (If I could gi…

> Also not a number theorist...but I'd bet those so-called experts had invested far, far too many of their man-years in that unproven conjecture. All of which effort and edifice would collapse into the dumpster if some snot-nosed little upstart like you, using crude computation, achieved overnight fame by finding a counter-example. Are you maybe confusing math academia for psychology or social sciences? There is no r…

Maths may not have a replication crisis like some other areas, but when I go to maths events, it seems widely agreed there are far too many papers with incorrect theorems, it's just no-one cares about those papers, so it doesn't matter.

It turns out to be very, very common (as discussed in the linked article) that when someone really carefully reads old papers, the proofs turn out to be wrong. They are often fixable, but the point of the paper was to prove the result, not just state it. What tends to save these papers is that enough extra results have been built on top of them, and (usually), if there had been an issue, it would have showed up as an inconsistency in one of the later results.

The trunk is (probably) solid, but there are a lot of rotten leaves, and even the odd branch.

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

#124

Post by jovas »

MrMcCall wrote: post #86

One of my favorite Horizon episodes is the FLT one that features Prof. Andrew Wiles' development of his proof (I have watched it many times). Of course, it is grounded in Fermat's margin note about his having a wonderful proof that couldn't fit in said margin. At the end of the documentary, the various mathematicians in it note that AW's proof certaintly wasn't what PdF had in mind because AW's proof is thorougly mod…

I believe Wiles' proof requires the case of n=3 (Euler), and n=4 (Fermat) separately. That is, Wiles' proof starts with n=5 for nontrivial reasons.

So it is more likely that Fermat saw n=4, and thought the rest would be similar.

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

#126

Post by devit »

impendia wrote: post #48
vouaobrasil wrote: post #24

> 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. Past researcher in pure math here. The big problem is that mathematicians are notorious for not providing self-contained proofs of anything because there is no incentive to do so and authors sometimes even seem proud to…

Speaking as a current researcher in pure math -- you're right, but I don't think this is easily resolved. Math research papers are written for other specialists in the field. Sometimes too few details are provided; indeed I commonly gripe about this when asked to do peer review; but to truly provide all the details would make papers far, far longer. Here is an elementary example, which could be worked out by anyone w…

I don't think that's a good example, since it's obviously provably true and the proof is also obvious (either use well-known lemmas like log(poly(x)) in O(x^a) or show that lim_x->inf lhs/x = 0 via L'Hôpital's rule, differentiation algorithms and well-known limits at infinity).

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

#127

Post by j16sdiz »

lambdaone wrote: post #20
coliveira wrote: post #6

Earlier quoted context omitted.

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

Reading these threads makes me feel oddly familiar. This is the same discussion we have with Rust:

"You can't write everything in safe rust, therefore rust is worthless." vs "You must throw away all C code, or the whole industry will collapse"

except we have thousands of years of "unsafe" math, only a few decades of C.

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

#128

Post by bandrami »

impendia wrote: post #48
vouaobrasil wrote: post #24

> 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. Past researcher in pure math here. The big problem is that mathematicians are notorious for not providing self-contained proofs of anything because there is no incentive to do so and authors sometimes even seem proud to…

Speaking as a current researcher in pure math -- you're right, but I don't think this is easily resolved. Math research papers are written for other specialists in the field. Sometimes too few details are provided; indeed I commonly gripe about this when asked to do peer review; but to truly provide all the details would make papers far, far longer. Here is an elementary example, which could be worked out by anyone w…

Is there really not a centralized corpus of that kind of fundamental result you guys can use? I would have assumed that was "theorem #44756" in a giant tome you all had in your bookshelf somewhere.

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

#129

Post by semolinapudding »

gedpeck wrote: post #64
jerf wrote: post #51

Earlier quoted context omitted.

That question contains so many false or unnecessary assumptions that it would take far longer to unpack them than it took you to type them, so I will limit myself to the observation that we do not even remotely confine ourselves to first order anything in computer science, nor should we.

What false assumption did I make? I just pointed out a fact and asked a question. How many false assumptions could I have made with just one statement of fact and two questions? If you don’t have a valid answer to the question then don’t respond. I’m a mathematician and not a computer scientist. The first order PA axioms are recursively enumerable. Hence it’s clearly something of interest to computer scientists. The…

The axioms of second order Peano arithmetic are certainly recursively enumerable, in fact you can pick a formulation that only uses a finite number of axioms. And second order arithmetic is much weaker than the type system of Lean, which is probably somewhere between Zermelo set theory and ZFC set theory in terms of proof-theoretic strength.

More generally, I think that computer scientists (in particular PL theorists and type theorists) are much more likely to use powerful logics than mathematicians, with the obvious exception of set theorists.

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

#130

Post by j16sdiz »

hughesjj wrote: post #113
sam_goody wrote: post #99

Richard Feynman, while still a student at Princeton, found an error in some well known proof, and set himself a rule to double check every theorem he would use. I don't remember the details of the story (I read surely your joking years ago), and remember being amazed by how much time that policy must have cost him. But now I wonder that he didn't hit dozens or hundreds of errors over the years.

I'd be careful taking anything from "surely you're joking" as a fact btw. There's a good popsci comms video on why here https://youtu.be/TwKpj2ISQAc?si=bpZOBy9WBGQzi6sk

She is more like complaining some (most?) RPF "bros" act like jerks, emotionally unstable, etc.

I guess the same can be said about many other "fanboi", and have little to do with the facts in the book

Post reply on HN