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

191–200 of 216 posts

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

#191

Post by naasking »

Tainnor wrote: post #190
naasking wrote: post #163

Earlier quoted context omitted.

> There are non-computable objects that mathematicians study. What's an example of such a non-computable object? Constructionism is based on the fact that every proof is a construction, which corresponds to a program, so you're claiming that there are proofs that do not correspond to any construction/program, and I'm curious what that might look like.

Constructivism is not mainstream mathematics. The theorem that every vector space has a basis, something that is used fairly often, is actually equivalent to the axiom of choice, something that isn't valid in constructive logic. For many vector spaces you won't be able to write down a basis. And there are other examples, e.g. almost none of the automorphisms of C can be written down (only the identity and the conjuga…

I'm aware that constructivism is not mainstream. What you've described are that such constructions are not available at this time (not comparable ones), but is there any evidence that comparable constructions are not possible even in principle?

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

#192

Post by wbl »

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 if you let C=3 it isn't that long. The first two terms are less than x for x>5, the last term is also less than x for all positive x, done. Those lemmas are pretty easy to figure out.

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

#193

Post by LegionMammal978 »

wbl wrote: post #192
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 think if you let C=3 it isn't that long. The first two terms are less than x for x>5, the last term is also less than x for all positive x, done. Those lemmas are pretty easy to figure out.

It's not that trivial if we really insist on all the details. Let's assume x > 0 throughout. We can take sqrt(x) An important lemma we need is that if f(x) is continuous on [a,b] and f'(x) > 0 on (a,b), then f(a) x/exp(sqrt(4x+3)) 1 = exp(0). Since sqrt(4x+3) > 0, we just need to show that exp(z) is increasing. For this, we can treat the exponential as the anti-logarithm (since that's how my high school textbook did it), then show that log(z) is increasing, which follows from log'(z) = 1/z > 0 and our lemma.

For log(x^2+1) f(0) = 0. Here, f'(z) = 1 - 2x/(x^2+1), for which we need the chain rule and the power rule (or a specialized epsilon–delta argument). Since x^2+1 > 0, f'(z) > 0 is implied by (x^2+1) - 2x > 0, which luckily factors into the trivial (x-1)^2 > 0. So ultimately, we break the lemma up into (0,1) and (1,x) to avoid trouble with the stationary point.

The trouble with problems like these is the whole foundation that the obvious lemmas have to be built upon. "Just look at the graph, of course it's increasing" isn't a rigorous proof. Of course, if you want to do this seriously, then you go and build that foundation, and on top of that you probably define some helpful lemmas for the ladder of asymptotic growth rates. But all of the steps must be written out at some point or another.

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

#194

Post by Atiscant »

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…

As mentioned by another comment, this is a big reason that Vladimir Voevodsky started his Homotopy Type Theory and Univalent Foundations program. He had see first hand a field collapse by a mistake in “first lemma on the first page” of a foundational paper. Arguably, he initial work on UniMath and the special year at IAS ending up in the HoTT book, pushed the whole formalization of mathematics topic forward to where it is today.

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

#195

Post by robinzfc »

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.

Isabelle proving environment implements this idea since at least 2005 when I started using it. One can interleave formal proofs and informal commentary in a theory file and one of the artifacts is a "proof document" that is a result of LaTeX processing of the file. Other options exist as well where the file is exported to HTML with hyperlinks to theorems and definitions referenced in a proof. There are also custom HTML renderers (since 2008) where a reader can expand parts of the structured proof when they want to see more details.

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

#196

Post by zozbot234 »

robinzfc wrote: post #195
jll29 wrote: post #115

Earlier quoted context omitted.

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.

Isabelle proving environment implements this idea since at least 2005 when I started using it. One can interleave formal proofs and informal commentary in a theory file and one of the artifacts is a "proof document" that is a result of LaTeX processing of the file. Other options exist as well where the file is exported to HTML with hyperlinks to theorems and definitions referenced in a proof. There are also custom HT…

Agda 1 (more specifically, the included UI program known as Alfa) implemented an automated translation from formal proof to natural language, driven via Grammatical Framework. This requires writing snippets of code to translate every single part of the formal language to its natural language equivalents, at varying levels of verboseness - for example, (add a b) could become "a + b", "the addition of a and b", "adding b to a" and so on. Similar for proof steps such as "We proceed by induction on n", properties such as "is commutative" etc. The idea gets reimplemented every now and then, in a variety of systems. Of course the most compelling feature is being able to "expand out" proof steps to any desired level of detail.

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

#197

Post by panda-giddiness »

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…

You might as well have written that mathematicians should stop doing mathematics. If every mathematician were to work full time on formalizing theorems in proof assistants, then no living mathematician would ever do original research again -- there is simply too much that would need to be translated to software. And to what end? It's not as if people suspect that the foundations of mathematics are on the verge of toppling.

> Code is easy to share, easy to collaborate on [...] collaboration is so easy that publishing your 1/2 done work will often prompt others to do some of the tedious stuff

Here's an experiment anyone can try at home: pick a random article from the mathematics arxiv [1]. Now rewrite the main theorem from that paper in Lean [2]. Did you find this task "easy"? Would you go out of your way to finish the "tedious" stuff?

> even horrible code is far better at documenting what it does than what you are describing

The "documentation" is provided by talking to other researchers in the field. If you don't understand some portion of a proof, you talk to someone about it. That is a far more efficient use of time than writing code for things that are (relatively) obviously true. (No shade on anyone who wants to write proofs in Lean, though.)

---

[1] https://arxiv.org/list/math/new

[2] https://lean-lang.org/theorem_proving_in_lean4/dependent_typ...

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

#198

Post by Tainnor »

naasking wrote: post #191
Tainnor wrote: post #190

Earlier quoted context omitted.

Constructivism is not mainstream mathematics. The theorem that every vector space has a basis, something that is used fairly often, is actually equivalent to the axiom of choice, something that isn't valid in constructive logic. For many vector spaces you won't be able to write down a basis. And there are other examples, e.g. almost none of the automorphisms of C can be written down (only the identity and the conjuga…

I'm aware that constructivism is not mainstream. What you've described are that such constructions are not available at this time (not comparable ones), but is there any evidence that comparable constructions are not possible even in principle?

Yes because the existence of a basis for arbitrary vector spaces is equivalent to the axiom of choice.

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

#199

Post by zozbot234 »

naasking wrote: post #163
gedpeck wrote: post #132

Earlier quoted context omitted.

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?

> There are non-computable objects that mathematicians study. What's an example of such a non-computable object? Constructionism is based on the fact that every proof is a construction, which corresponds to a program, so you're claiming that there are proofs that do not correspond to any construction/program, and I'm curious what that might look like.

> Constructionism is based on the fact that every proof is a construction, which corresponds to a program

I don't think this is correct, even in constructive logic. Negative statements do not correspond to a construction, and in fact are the only statements in constructive logic that may be proven "by contradiction". But this means that every statement of non-constructive logic can be understood "constructively", if in a rather trivial sense, as a negative statement.

Linear logics may be a good way of exploring these issues in depth, since these allow for explicit "constructions" while preserving the sort of 'duality of negation' (i.e. flipping the direction of implications, or exchanging conjunctions w/ disjunctions) that's quite familiar within classical logic. Somewhat relatedly, there's also an interesting question of how much "construction" really is involved in typical constructive proofs, and whether that can be cleanly separated out from the more purely "logical" parts of the proof.

Post reply on HN