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

141–150 of 216 posts

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

#141

Post by ykonstant »

zyklu5 wrote: post #65
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.

No, I am not an expert of 4-manifold theory and would not really understand most of the chapters. If this book fixes some of the literature issues in that field that is amazing! Does it finally resolve the issue of nobody understanding the construction of topological Casson handles?

Edit: I see from the MO comments "The fully topological version of the disc embedding theorem is beyond the scope of this book, since we will not discuss Quinn's proof of transversality."

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

#142

Post by ykonstant »

eab- wrote: post #122
rstuart4133 wrote: post #93

Earlier quoted context omitted.

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

I agree, although I don't see a better solution: typeclass inference is trying to "quasi-solve" higher unification, which is unsolvable. The core tactics writers are already doing wizard-level stuff and there is more to come, but the challenge is immense.

By the way, if you are a meta-programming wizard and/or a Prolog wizard, please consider learning Lean 4 or another tactics based proof assistant. I think they will all welcome expert assistance in the development of better tactics and the improvement and debugging of current ones.

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

#143

Post by ykonstant »

jll29 wrote: post #115
vouaobrasil wrote: post #54

Earlier quoted context omitted.

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

This is already happening, by the way, and some Lean projects are being written in this way. Not only for the reader, but the proof writers themselves tend to need this to navigate their own code. Also check Lean 4 Blueprint, which is a component in this direction.

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

#144

Post by NooneAtAll3 »

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.

"the proof is trivial"

"but can you prove it?

[10 minutes of intense staring and thinking]

"yes, it is trivial"

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

#146

Post by mrintegrity »

boothby wrote: post #27

This reminds me of a fun experience I had in grad school. I was working on writing some fast code to compute something I can no longer explain, to help my advisor in his computational approach to the Birch and Swinnerton-Dyer conjecture. I gave a talk at a number theory seminar a few towns over, and was asked if I was doing this in hopes of reinforcing the evidence behind the conjecture. I said with a grin, "well, no…

> The crowd went wild

I am curious what a group of number theorists "going wild" looks like.. were they throwing chairs or are we talking slightly raised eyebrows?

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

#147

Post by hughesjj »

j16sdiz wrote: post #130
hughesjj wrote: post #113

Earlier quoted context omitted.

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

No, she's claiming that most of those stories were made up by a third guy with Daddy issues (if you want to be reductive)

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

#148

Post by cha42 »

boothby wrote: post #59
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…

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

Recently I found myself happy to find bug in code I have writtdn for those reasons.

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

#149

Post by rocqua »

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 think the resolution is being much less strict on paper appendix size. And slightly shortening the main body of a paper. Let the main text communicate to the experts. Let the appendix fill things in for those looking to learn, and for the experts who are sceptical.

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

#150

Post by semolinapudding »

gedpeck wrote: post #131
semolinapudding wrote: post #129

Earlier quoted context omitted.

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…

Do you have a reference for the second order induction schema being recursively enumerable? My understanding - I’m not a logician - is that the second order Peano Axioms are categorical. The Incompleteness theorems don’t apply to this system since the axioms are not recursively enumerable. The second order Axioms are different than second order Arithmetic. https://mathoverflow.net/questions/97077/z-2-versus-second-o.…

If you look at the Wikipedia page for second order arithmetic, there is a definition in the language of first order logic as a two-sorted theory comprising a handful of basic axioms, the comprehension scheme, and the second-order induction axiom (in your first mathoverflow link, this is called Z_2):

https://en.wikipedia.org/wiki/Second-order_arithmetic#The_fu...

An other equivalent option would be to use the language of second order logic, where you only need a finite amount of axioms, because the comprehension scheme is already included in the rules of second order logic. This one is PA_2.

Since these definitions do not refer to anything uncomputable such as mathematical truth, both systems are clearly recursively enumerable. This means that Gödel's incompleteness theorem applies to both, in the sense that you can define a sentence in the language of arithmetic that is unprovable in Z_2 or PA_2, and whose negation is also unprovable.

All of these considerations have little to do with models or categoricity, which are semantic notions. I think your confusion stems from the fact that model theorists have the habit of using a different kind of semantics for Z_2 (Henkin semantics) and PA_2 (full semantics). Henkin semantics are just first order semantics with two sorts, which means that Gödel's completeness theorem applies and there are nonstandard models. Full semantics, on the other hand, are categorical (there is only one model), but this has nothing to do with the axioms not being recursively enumerable -- it is just because we use a different notion of model.

PS: I certainly do not consider mathematics to be included in computer science. Even though as a logician, I have been employed in both mathematics departments and computer science departments...

Post reply on HN