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

131–140 of 216 posts

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

#131

Post by gedpeck »

semolinapudding wrote: post #129
gedpeck wrote: post #64

Earlier quoted context omitted.

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…

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

In the following mathoverflow answer Nik says,

These are fundamental questions. We know that any computable set of axioms which holds of the natural numbers must also have nonstandard models.

The second order Peano Axioms are not computable since those axioms are categorical.

https://mathoverflow.net/questions/332247/defining-the-stand...

Are you of the opinion that mathematics is computer science? I have a hard time believing that the Jacobian Conjecture is computer science.

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

#132

Post by gedpeck »

immibis wrote: post #100
gedpeck wrote: post #64

Earlier quoted context omitted.

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…

why should computer science be limited to things that are first order PA?

It shouldn’t and I didn’t say it should. I gave a fact and asked a question. Why is PA_2 computer science?

Computer science ought to be about computation, right? There are non-computable objects that mathematicians study. Is that part of computer science?

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

#133

Post by rendaw »

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…

I have no background in math, so this might be naive, but shouldn't proof checkers have a database of theorems and be able to fill in the intermediate steps or confirm that it's possible to fill in the missing steps?

IIUC you're saying that basically someone with a mental database should be able to identify preconditions matching some theorem and postconditions aligned with the next statement from their mental database.

Or is there math that can't be expressed in a way for proof checkers to assess atm?

Edit: Or maybe proof checker use just isn't as wide-spread as I imagined. It sounds like the state statically typed languages in programming...

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

#134

Post by bubblyworld »

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…

I think it depends how widely used that branch of maths becomes. In fact, I'd say that the word "branch" is a bit misleading - for many theories it's much more of a "knot", with influences tying them to many many other theories across the mathematical landscape. And those theories are themselves tied to others, etcetera.

It would be a very strange situation if the foundation fell apart logically without any ramifications in the rest of this "knot". A huge swathe of free-floating mathematics that's completely internally consistent but for this one error? Difficult to imagine for me in the case of cohomology from the article.

I guess strictly speaking this is more of a philosophical stance - I like to believe that a lot of the current mathematics has been discovered "naturally" in some sense =)

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

#135

Post by williamstein »

williamstein wrote: post #82
rateofclimb wrote: post #72

Earlier quoted context omitted.

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! :)

I took that class with you! It was amazing. Here are my notes: https://wstein.org/books/ribet-stein/

And the professor who taught that course won a major prize today: Ribet to Receive 2025 AMS Steele Prize for Seminal Research - https://www.ams.org/news?news_id=7391&fbclid=IwZXh0bgNhZW0CM...

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

#136

Post by lmm »

XorNot wrote: post #105
baruz wrote: post #83

Earlier quoted context omitted.

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.

The worst part of middle-class life in the US is its precariousness. A guaranteed lower middle-class living for life is a pearl indeed.

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

#137

Post by gjm11 »

bell-cot wrote: post #73
baruz wrote: post #62

Earlier quoted context omitted.

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

What exactly are you saying this is an example of?

It's certainly not something that people believed and built stuff on the basis of; it was never regarded as anything more than a conjecture and I would be a little surprised if even one paper was published that took the conjecture as a hypothesis, even explicitly (i.e., "We show that if Euler's conjecture is true then ...").

It's also not, so far as I know, a case where anyone reacted with defensiveness, horror, insecurity, etc., when a counterexample was found. They published a paper in a reputable journal. They don't seem to have had much trouble getting it published, if they discovered the counterexample in 1966 and the paper was published in a 1966 issue of said journal.

So if you're suggesting that this is a case where "people were building on swathes of mathematics that seem proven and make intuitive sense, but needed formal buttressing", I'd like to see some evidence. Same if you're suggesting that this is a case where "so-called experts had invested far, far too many of their man-years in that unproven conjecture" and there'd be a hostile reaction to a counterexample.

On the other hand, if you're not suggesting either of those things, I'm not sure what the connection to the rest of the discussion is.

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

#138

Post by awanderingmind »

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…

> [...]this article shows that our anxiety at the perceived lack of formalism is justified, but we must remember that anxiety is a feeling -- and the proper response to that feeling is curiosity, not avoidance.

Beautiful sentiment, also in other areas of life, thank you.

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

#139

Post by JulianWasTaken »

rendaw wrote: post #133
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…

I have no background in math, so this might be naive, but shouldn't proof checkers have a database of theorems and be able to fill in the intermediate steps or confirm that it's possible to fill in the missing steps? IIUC you're saying that basically someone with a mental database should be able to identify preconditions matching some theorem and postconditions aligned with the next statement from their mental databa…

> shouldn't proof checkers have a database of theorems and be able to fill in the intermediate steps or confirm that it's possible to fill in the missing steps?

This is essentially exactly what Mathlib[1] is, which is Lean's database of mathematics, and which large portions of the FLT project will likely continually contribute into.

[1]: https://github.com/leanprover-community/mathlib4/

(Other theorem provers have similar libraries, e.g. Coq's is called math-comp: https://math-comp.github.io/ )

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

#140

Post by plank »

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

Not a (former) mathematicien (but as a former PhD student in theoretical physics still some affinity with math): I remember being shocked when, having derived a result using pen and lots of sheets of paper, my co-promotor told me to just write ' can be rewritten as ' and only briefly explaining how (nothing more then a line or two), as the magazine we were to publish (and did publish) the article would not want any of those calculations written out.
Post reply on HN