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

61–70 of 216 posts

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

#61

Post by ykonstant »

impendia wrote: post #60
ykonstant wrote: post #55

Earlier quoted context omitted.

The example you gave, however, is obvious to every graduate student in any field that touches analysis or asymptotics. That is not the real problem; the real problem is proof by assertion of proof: "Lemma 4.12 is derived by standard techniques as in [3]; so with that lemma in hand, the theorem follows by applying the arguments of Doctorberg [5] to the standard tower of Ermegerds." Too many papers follow this pattern,…

I strongly agree with you, in the sense that many papers provide far fewer details than they should, and reading them is considered something of a hazing ritual for students and postdocs. (I understand that this is more common in specialties other than my own.) The blog post seems to be asserting a rather extreme point of view, in that even the example I gave is (arguably!) unacceptable to present without any proof.…

> (I understand that this is more common in specialties other than my own.)

True, analytic number theory does have a much better standard of proof, if we disregard some legacy left from Bourgain's early work.

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

#62

Post by baruz »

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…

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

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

#63

Post by impendia »

zozbot234 wrote: post #57
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…

> there exist constants C, X > 0 such that for every real number x > X, we have >> log(x^2 + 1) + sqrt(x) + x/exp(sqrt(4x + 3)) These problems are only "uninteresting" to the extent that they can be "proven" by automated computation. So the interesting part of the problem is to write some completely formalized equivalent to a CAS (computer algebra system - think Mathematica or Maple, although these are not at all fre…

The problems are uninteresting in the sense that the audience for these papers doesn't find them interesting.

In particular, I'm not making any sort of logical claim -- rather, I know many of the people who read and write these papers, and I have a pretty good idea of their taste in mathematical writing.

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

#64

Post by gedpeck »

jerf wrote: post #51
gedpeck wrote: 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.

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 second order PA axioms aren’t so…are they part of computer science? What do computer scientists think about proofs in second order PA? There are no computable models of ZFC so wouldn’t it be the case that while computer scientists deal with ZFC that ZFC isn’t part of computer science? what is your definition of computer science? Physicists deal with a vast amount of mathematics but math isn’t physics. In the same way mathematics isn’t computer science.

Overall I think most mathematicians would not consider mathematics as part of computer science.

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

#65

Post by zyklu5 »

ykonstant wrote: post #30

I am extremely disappointed at the replies from (some) experts. As a mathematician who has been worrying about the state of the literature for some time, I expected trouble like this---and expect considerably more, especially from the number theory literature between the 60s and the 90s. I also wonder how well 4-manifold theory is faring. Much worse, this nonchalant attitude is being taught to PhD students and postdo…

Re: that dig at 4-manifolds

Are you aware of the book on [The Disc Embedding Theorem](https://academic.oup.com/book/43693) based on 12 lectures Freedman gave roughly a decade ago.

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

#66

Post by zozbot234 »

impendia wrote: post #63
zozbot234 wrote: post #57

Earlier quoted context omitted.

> there exist constants C, X > 0 such that for every real number x > X, we have >> log(x^2 + 1) + sqrt(x) + x/exp(sqrt(4x + 3)) These problems are only "uninteresting" to the extent that they can be "proven" by automated computation. So the interesting part of the problem is to write some completely formalized equivalent to a CAS (computer algebra system - think Mathematica or Maple, although these are not at all fre…

The problems are uninteresting in the sense that the audience for these papers doesn't find them interesting. In particular, I'm not making any sort of logical claim -- rather, I know many of the people who read and write these papers, and I have a pretty good idea of their taste in mathematical writing.

Well, you did claim that the problem could be worked out with simply high school math. It would certainly be 'interesting' if such problems could not be answered by automated means.

(For example, I think many mathematicians would find the IMO problems interesting, even though the statements are specifically chosen to be understandable to high-school students.) The problem of how to write an automated procedure that might answer problems similar to the one you stated, and what kinds of "hints" might then be needed to make the procedure work for any given instance of the problem, is also interesting for similar reasons.

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

#67

Post by zellyn »

ykonstant wrote: post #55
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…

The example you gave, however, is obvious to every graduate student in any field that touches analysis or asymptotics. That is not the real problem; the real problem is proof by assertion of proof: "Lemma 4.12 is derived by standard techniques as in [3]; so with that lemma in hand, the theorem follows by applying the arguments of Doctorberg [5] to the standard tower of Ermegerds." Too many papers follow this pattern,…

I think Kevin Buzzard et al are aiming for a future where big, complicated proofs not accompanied by code are considered suspicious.

I wonder if being able to drill all the way down on the proof will alleviate much of the torture you mention.

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

#68

Post by staunton »

lincolnq wrote: post #9

If you're interested in this stuff at all, check out some code. Example: https://github.com/ImperialCollegeLondon/FLT/blob/main/FLT/M... Also check out the blueprint, which describes the overall structure of the code: https://imperialcollegelondon.github.io/FLT/blueprint/ I'm very much an outside observer, but it is super interesting to see what Lean code looks like and how people contribute to it. Great thing is tha…

Most (larger) Lean projects still have "unit tests". Those might be, e.g., trivial examples and counter examples to some definition, to make sure it isn't vacuous.

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

#69

Post by pfdietz »

hyperthesis wrote: post #44
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…

There'a a story that when someone wrote up a famous mathematician's work (Euler?), he found many errors, some quite serious. But all the theorems were true anyway. Sounds like Tao's third stage, of informed intuition.

Back in Euler's time there as a lot of informality. The rigor of the second half of the 19th century was still some time in the future.

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

#70

Post by staunton »

modeless wrote: post #40

> 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.
Post reply on HN