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

101–110 of 216 posts

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

#101

Post by adrian_b »

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

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 determine the title of the quoted book or research paper or the name of the publication in which it was included, and googling does not find any plausible match for those abbreviations.

In such cases it becomes impossible to verify the content of the paper that is read.

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

#103

Post by zozbot234 »

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.

This is not an easy change at all. Some subfields of math rely on a huge amount of prereqs, that all have to be formalized before current research in that field can insist on formal proofs for everything as a matter of course. This is the problem that the Lean mathlib folks are trying to address, and it's a whole lot of work. The OP discusses a fraction of that work - namely, formalizing every prereq for modern proofs of FLT - that is expected to take several years on its own.

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

#105

Post by XorNot »

baruz wrote: post #83
mostly_a_lurker wrote: post #75

Earlier quoted context omitted.

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

Does this not imply that /u/bell-cot had been a graduate student in mathematics? > If I could give my many-decades-ago younger self some advice for math grad school

It's HN bread-and-butter to insist that all experts are wrong, and it must be because BIG is just protecting the sweet sweet lower middle-class living of being a tenured professor or something.

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

#106

Post by XorNot »

adrian_b wrote: post #101
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,…

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 conventional citation backstopping that the hash and author intent and target all match.

But that runs directly into the problem of how the whole system is commercialized (although at least requiring publishers to hold proofs they have a particular byte-match for a paper on file would be a start).

Basically we have a system which is still formatted around the limitations of physical stacks of A4/Letter size paper, but a scientific corpus which really is too broad to only exist in that format.

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

#108

Post by zozbot234 »

jebarker wrote: post #102

Formalization of maths seems like an overwhelmingly huge task. A bit like Cyc but harder. Is there some kind of chain reaction likely to happen once a critical mass of math has been formalized so that it becomes easier to do more?

If anything, it's a relatively straightforward way to do what amounts to publishable work in mathematics. Besides the obvious point of being able to claim "I've dotted all the i's and crossed all the t's", formalized proofs are often more elegant than the original they're based on because refactoring a proof to be simpler, more general etc. and checking that it still goes through is comparatively easy - and obviously, mathematicians are interested in that.

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

#109

Post by hughesjj »

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.

It's still incredibly painful as a learner though when things don't quite pan out. You start gaslighting yourself and then handwaved/convince yourself away that this must be true given how consistent all the "downstream" work is, and that you just don't fully understand it.

So, I agree with the author that this is super helpful, even if we know the proofs are "true" in the end

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

#110

Post by hughesjj »

dogboat wrote: post #91
TechDebtDevin wrote: post #42

Earlier quoted context omitted.

I don't even understand how you interpreted that to have anything to do with being "smarter or making more money". Get some more coffee dude.

Maybe less coffee :)

But how else would I power this machine that outputs theorems?
Post reply on HN