Live data from Hacker News

Fermat's Last Theorem – how it’s going

xenaproject.wordpress.com

71–80 of 216 posts

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

#72
post #43

I remember when I was a student a friend of mine telling me this guy was giving a seminar and he'd just completed day one and everyone was really excited he was going to prove FLT. Of course, the guy in question was Andrew Wiles. He then spent months patching up problems they found prior to publication and finally the whole thing got published. It was a hugely exciting thing when you were studying mathematics. All of…

As a CS undergrad at Berkeley in the 90's I took an upper division math class in which we worked through the "old school" proof which was brand new and exciting then. Pretty much everyone else in the class was a math grad student. I don't think I understood more than 20% of the material! :)

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

#73
post #62

Earlier quoted context omitted.

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

> no house of cards As I understand TFA, from a formalist’s perspective, this is not necessarily the case. People were building on swathes of mathematics that seem proven and make intuitive sense, but needed formal buttressing. > _actually experts_ at a deep and rigorous technical field Seeing as the person you’re addressing was a mathematics graduate student, I’m sure they know this.

Yep. Here's an easy-looking one, that lasted just under 2 centuries (quoting Wikipedia) -

> In number theory, Euler's conjecture is a disproved conjecture related to Fermat's Last Theorem. It was proposed by Leonhard Euler in 1769. It states that for all integers n and k greater than 1, if the sum of n many kth powers of positive integers is itself a kth power, then n is greater than or equal to k...

> ...

> Euler's conjecture was disproven by L. J. Lander and T. R. Parkin in 1966 when, through a direct computer search on a CDC 6600, they found a counterexample for k = 5.[3] This was published in a paper comprising just two sentences.[3]

> [3] - Lander, L. J.; Parkin, T. R. (1966). "Counterexample to Euler's conjecture on sums of like powers". Bull. Amer. Math. Soc. ...

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

#74
Haha, that author is a funny writer. Very weird experience for that to be so readable, when I didn't understand probably half the content.

By the way, I found an excellent word for when a proof is disproven or found to be faulty, but that is esoteric enough that it has less risk of being misinterpreted to mean the conclusion is proven false: 'vitiated'. The conclusion might still be true, it just needs a new or repaired proof; the initial proof is 'vitiated'. I like how the word sounds, too.

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

#75
post #62

Earlier quoted context omitted.

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

> no house of cards As I understand TFA, from a formalist’s perspective, this is not necessarily the case. People were building on swathes of mathematics that seem proven and make intuitive sense, but needed formal buttressing. > _actually experts_ at a deep and rigorous technical field Seeing as the person you’re addressing was a mathematics graduate student, I’m sure they know this.

> Seeing as the person you’re addressing was a mathematics graduate student, I’m sure they know this.

The OP (u/boothby) was not the person I was addressing (u/bell-cot).

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

#76
post #51
post #25

Earlier quoted context omitted.

There are statements provably true about the natural numbers that can’t be proven in first order PA. Are such statements part of computer science? If so, how?

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.

>it would take far longer to unpack them than it took you to type them

Why is this a barometer for whether to answer a question or unpack assumptions?

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

#77

> it was absolutely clear to both me and Antoine that the proofs of the main results were of course going to be fixable, even if an intermediate lemma was false, because crystalline cohomology has been used so much since the 1970s that if there were a problem with it, it would have come to light a long time ago. I've always wondered if this intuition was really true. Would it really be so impossible for a whole branc…

This has happened before, see, e.g. the biography of Vladimir Voevodsky. Spoiler: the world kept spinning.

Russell’s paradox did the same thing. They had to go back to the drawing board.

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

#78

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…

To put a little color on the BSD conjecture, it states that the rank (0, 1, 2, 3, etc.) of rational points on an elliptic curve is related to the residue (coefficient of 1/q) of the L-function for the curve. There are some additional multiplicative factors, in particular the size of the Tate-Shafarevich group. No one knows how to compute the size of that group in general (in fact no one has proved that it's finite!).…

If the BSD rank conjecture were false, then the simplest counterexample might be an elliptic curve with algebraic rank 4 and analytic rank 2. This could be established for a specific curve by rigorously numerically computing the second derivative of the L-series at 1 to some number of digits and getting something nonzero (which is possible because elliptic curves are modular - see work of Dikchitser). This is a straightforward thing to do computations about and there are large tables of rank 4 curves. This is also exactly the problem I suggested to the OP in grad school. :-)

In number theory doing these sorts of “obvious computational investigations” is well worth doing and led to many of the papers I have written. I remember doing one in grad school and being shocked when we found a really interesting example in minutes, which led to a paper.

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

#79

Haha, that author is a funny writer. Very weird experience for that to be so readable, when I didn't understand probably half the content. By the way, I found an excellent word for when a proof is disproven or found to be faulty, but that is esoteric enough that it has less risk of being misinterpreted to mean the conclusion is proven false: 'vitiated'. The conclusion might still be true, it just needs a new or repai…

Perhaps more delightful to the ears to hear that a proof has been disemboweled.

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

#80
post #17

This makes me wonder if there'll ever be a significant bug discovered in Lean itself, breaking past formalisation work.

For the problem to affect proofs, it would have to be in the type checker, and the type system isn’t really that complex. The good news is that every single user of Lean checks this works every day. Finding a flaw that literally everyone relies upon and doesn’t notice is pretty implausible.
Post reply on HN