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

201–210 of 216 posts

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

#201

Post by subsistence234 »

bell-cot wrote: post #172
gjm11 wrote: post #137

Earlier quoted context omitted.

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

> What exactly are you saying this is an example of? A prominent conjecture in number theory, taken quite seriously for centuries, but which was quickly and rather easily disproven once computers became powerful enough. No, it is not a exact analogy for Fermat, nor BSD, nor Riemann, nor ... My initial point of interest was u/bootby's comment - why the heck would a room full of experts (presumably noteworthy math prof…

they didn't become angry, they became excited.

and a famous conjecture is by definition something for which all the experts know that its truth is UNKNOWN (even in cases where most experts believe it's true).

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

#202

Post by naasking »

Tainnor wrote: post #198
naasking wrote: post #191

Earlier quoted context omitted.

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.

A derivation of the axiom of choice in Martin-Löf Type Theory, which is constructive:

https://plato.stanford.edu/entries/axiom-choice/choice-and-t...

This is exactly what I'm talking about, "every vector space has a basis" is not a provable statement in constructive mathematics because that ranges over non-constructive objects, but it can prove constructive equivalents like "every finite-dimensional or countable vector space has a basis".

I'm just not persuaded that this is not sufficient for any realizable mathematical construction. In my view, some non-constructive objects are non-realizable and so must ultimately serve only as convenient shortcuts that are ultimately eliminated when the math manifests in a real construction, either physical or computational. So if such things are merely artifacts of a particular formalism, then it should be possible to dispense with them entirely with a constructive or intuitionistic formalism.

That's why I'm looking for something that truly, fundamentally impossible for constructive mathematics, but that we know to exist, be true, valid, etc. that would contradict this position.

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

#203

Post by naasking »

zozbot234 wrote: post #199
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.

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

You're right that I'm being a little loose with terminology, as when I say "constructivism" I mean something more like "intuitionism", as with type theory.

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

#204

Post by zozbot234 »

naasking wrote: post #203
zozbot234 wrote: post #199

Earlier quoted context omitted.

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

You're right that I'm being a little loose with terminology, as when I say "constructivism" I mean something more like "intuitionism", as with type theory.

Intuitionistic logic also allows for negative statements, which then are entirely non-constructive.

From a proofs-as-programs POV, this is just the observation that a proof is not just a program, but rather a program plus an explanation of why that program works correctly within its constraints, e.g. why it never ever tries to divide by zero. (This can be rephrased by saying that the program is both requesting and providing abstract "capabilities", i.e. information-free tokens, to its environment. Classical logic is then the logic of these capabilities, in the sense that providing a weak capability as output is essentially the same as asking for a strong capability from your environment as input.)

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

#207

Post by anthk »

naasking wrote: post #162
pkoird wrote: post #21

Earlier quoted context omitted.

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

> I'd argue for the converse: Computer Science is Mathematics The space of programs is arguably larger than the space of mathematical systems, because programs can be logically inconsistent. This suggests that mathematics is a logically consistent subset of computer science, not the other way around.

And then you are wrong because everything now theorized into CS was already a thing in Math since long ago.

Lisp? Knuth and computation? Lambda Calculus did it before. ] https://en.m.wikipedia.org/wiki/Lambda_calculus

And, before computers, we had these:

https://en.m.wikipedia.org/wiki/State_machine

https://en.m.wikipedia.org/wiki/Control_theory

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

#208

Post by saghm »

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…

> Edit 2: This attitude pervades my software development career, and I've brought it to my foray into superconducting circuit design: a bug report brings joy to my life, and I aim to shower the reporter with praise (which may involve chocolate). There is nothing more satisfying than being proven wrong, because it helps us collectively move toward greater truths.

Not to mention that the usual wisdom of "don't kill the messenger" applies equally to bug reporters! Someone finding a bug in your code doesn't mean they willed it into existence; the bug would still be there even if you didn't know about it.

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

#209

Post by norlygfyd »

munchler wrote: post #85
Retr0id wrote: post #17

This makes me wonder if there'll ever be a significant bug discovered in Lean itself, breaking past formalisation work.

Lean has a small “kernel” that has been independently checked multiple times, and the rest of Lean depends on the kernel. A soundness bug is still possible, but pretty unlikely at this point. https://lean-lang.org/lean4/doc/faq.html

Soundness of Lean requires more than correctness of the kernel - it requires that the theory be sound. That, frankly, is a matter of mathematics folklore. "It is known" that the combination of rules Lean uses is sound... unless it isn't.

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

#210

Post by munchler »

norlygfyd wrote: post #209
munchler wrote: post #85

Earlier quoted context omitted.

Lean has a small “kernel” that has been independently checked multiple times, and the rest of Lean depends on the kernel. A soundness bug is still possible, but pretty unlikely at this point. https://lean-lang.org/lean4/doc/faq.html

Soundness of Lean requires more than correctness of the kernel - it requires that the theory be sound. That, frankly, is a matter of mathematics folklore. "It is known" that the combination of rules Lean uses is sound... unless it isn't.

That would be a bug in math itself, rather than a bug in Lean. It's possible, of course, but even less likely.
Post reply on HN