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

111–120 of 216 posts

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

#111

Post by jebarker »

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

The refactoring idea is interesting because I can imagine "proof compression" creating a less readable proof too, similarly to how a code one liner can be harder to read.

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

#113

Post by hughesjj »

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

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

#114

Post by hughesjj »

practal wrote: post #81
pkoird wrote: post #21

Earlier quoted context omitted.

I'd argue for the converse: Computer Science is Mathematics

Let's just say there is a really big overlap between the two. And each one can learn from the point of view of the other.

Then we have the ghosts of information and category theories underpinning/influencing them all (including physics) (to some degree)

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

#115

Post by jll29 »

vouaobrasil wrote: post #54
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…

> but to truly provide all the details would make papers far, far longer. I think what we need in math is that eventually, a collection of frequently cited and closely related papers should be rewritten into a much longer book format. Of course some people do that, but they hardly get much credit for it. It should be much more incentivated, and a core part of grant proposals.

Donald Knuth's literate computing could be an example to follow:

combine lean prove language with inline English human language that explains it. Then, Lean files can be fed into Lean to check the proof, and LaTeX files can be fed into LaTeX to produce the book that explains it all to us mere mortals.

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

#116

Post by jll29 »

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…

DOIs fix that.

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

#117

Post by hughesjj »

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…

To be fair I've heard gripes about statistics, and sometimes even probability being considered as part of mathematics.

The lines between (academic) fields are blurry -- academic fields do not form a set theoretic partitioning over areas of study.

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

#118

Post by boothby »

setopt wrote: post #97
boothby wrote: post #59

Earlier quoted context omitted.

> 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. Not at all . In fact, if I had found a counterexample, it would cause a flurry of new research to quantify exactly how wrong the BSD conjecture is. Such a finding would actually be a boon to their career! That's why my response is…

> my foray into superconducting circuit design Curious, what do you work on? (I also research superconductivity.)

I've got a brief bio in my profile. The major thrust of my role is to develop architectures of digital/analog circuits for quantum computers, and I've lately been getting into device design. That's miles away from superconductivity research (at most, I could say I'm in applied superconductivity), so allow me to fawn a little... I'd love to be doing that kind of work!

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

#119

Post by blackenedgem »

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.

You may want to watch this if Surely You're Joking read years ago is your main reference point: https://youtu.be/TwKpj2ISQAc

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

#120

Post by wbl »

brap wrote: post #84
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…

>Here is an elementary example, which could be worked out by anyone with a good background in high school math WTF >i.e. the left-side is big-O of the right. Oh.

Calc AB covers it, and BC certainly gives you enough for a proof.
Post reply on HN