Live data from Hacker News

Fermat's Last Theorem – how it’s going

xenaproject.wordpress.com

31–40 of 216 posts

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

#31

This hurts my engineer-brain. Just a reminder than the gap between us and mathematicians is about the same as the gap between us and everybody else (edit: in terms of math skills), just in the other direction, haha. Oh well, hopefully when they get the machines to solve math, they’ll still want them to run a couple percents faster every year.

> about the same as the gap between us and everybody else My bet: there is a very long list of skills for which the gap between you and a person randomly picked out the whole population is very large, and not in the direction you seem to think.

That’s true. It was poor phrasing on my part. But I do realize I’m really bad at a ton of things. I just meant in the math context.

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

#32

This hurts my engineer-brain. Just a reminder than the gap between us and mathematicians is about the same as the gap between us and everybody else (edit: in terms of math skills), just in the other direction, haha. Oh well, hopefully when they get the machines to solve math, they’ll still want them to run a couple percents faster every year.

[flagged]

I just meant in the context of math skills, but I definitely acknowledge that it was poor phrasing on my part.

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

#33

Earlier quoted context omitted.

> consider getting mathematics written down properly, i.e. in a formal system This was already tried, and failed (Hilbert). In the aftermath of the failure we learned that mathematics cannot be completely formalized. So this points to a fundamental problem with using AI to do math.

While it's true that mathematics cannot ever be completely formalized, per Gödel's incompleteness theorems, a huge amount of it obviously can, as is demonstrated by the fact that we can write it down in a reasonably rigorous way in a combination of conventional mathematical notation and plain English. Nor is this in any way "a fundamental problem with using AI to do math".

It's a fundamental problem with using AI to do "intuitive" math, but not a fundamental problem with AI to do formal math.

As you have stared, a lot of mathematics can be formalized. For me the problem for AI with math is going to be the generative part. Validating a proof or trying to come up with a proof for a given statement may be within reach. Coming up with meaningful/interesting statements to proof is another completely different story.

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

#34

This hurts my engineer-brain. Just a reminder than the gap between us and mathematicians is about the same as the gap between us and everybody else (edit: in terms of math skills), just in the other direction, haha. Oh well, hopefully when they get the machines to solve math, they’ll still want them to run a couple percents faster every year.

Just a gentle reminder from somebody with a foot in each camp: computers were invented by mathematicians to accelerate computation. The field of Computer Science is a child of the field of Mathematics. Computer Engineering is its grandchild.

And yes, the desire for formalism has been stronger in the descendants than the ancestors for some time, but we're seeing that gap close in real time and it's truly exciting.

And, lets keep pushing the frontier of computation! We aren't just making better ad-delivery devices.

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

#35

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…

One of the best things about proof assistants is that they're not convinced by how "obvious" you think something is. It's much harder for a human to resist proof by social forces such as intimidation, confidence, and "it's well known".

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

#36

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

Studied math a long time ago and one of my profs was proud about not going into the details. He said "Once you did something 100 times, you can go and say -as easily observable- and move on."

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

#37

> This story really highlights, to me, the poor job which humans do of documenting modern mathematics. There appear to be so many things which are “known to the experts” but not correctly documented. 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. For me, this is just…

> consider getting mathematics written down properly, i.e. in a formal system This was already tried, and failed (Hilbert). In the aftermath of the failure we learned that mathematics cannot be completely formalized. So this points to a fundamental problem with using AI to do math.

Hilbert's program assumed math to be completely decidable, i.e. that for every possible statement, a decision procedure could tell whether it was true or false. We know now that no such procedure can possibly exist. But merely writing down all known math in a formal system is completely doable. (Of course, formalization systems can be used to state any additional axioms that may be required of any given argument or development, so the original concerns about incompleteness are just not very relevant.)

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

#38
post #36

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

Studied math a long time ago and one of my profs was proud about not going into the details. He said "Once you did something 100 times, you can go and say -as easily observable- and move on."

I loved that some of the proof solutions in the back of mathematical logic book said, "Observe that ..." as the start of the proof. Our little study group definitely did not see how what followed was an observation we would have made.

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

#39

Earlier quoted context omitted.

> consider getting mathematics written down properly, i.e. in a formal system This was already tried, and failed (Hilbert). In the aftermath of the failure we learned that mathematics cannot be completely formalized. So this points to a fundamental problem with using AI to do math.

While it's true that mathematics cannot ever be completely formalized, per Gödel's incompleteness theorems, a huge amount of it obviously can, as is demonstrated by the fact that we can write it down in a reasonably rigorous way in a combination of conventional mathematical notation and plain English. Nor is this in any way "a fundamental problem with using AI to do math".

There are two problems with this.

First, writing something down in English is very different from formalizing it. Natural language interacts with human brains in all kinds of complicated ways that we do not fully understand, so just because we can make a compelling-sounding argument in English doesn't mean that argument doesn't have holes somewhere.

Second, the incompleteness theorems apply only to given formal systems, not to formality in general. Given a system, you can produce a Godel sentence for that system. But any Godel sentence for a given system has a proof in some other more powerful system. This is trivially true because you can always add the Godel sentence for a system as an axiom.

This is a very common misconception about math even among mathematicians. Math produces only conditional truths, not absolute ones. All formal reasoning has to start with a set of axioms and deduction rules. Some sets of axioms and rules turn out to be more useful and interesting than others, but none of them are True in a Platonic sense, not even the Peano axioms. Natural numbers just happen to be a good model of certain physical phenomena (and less-good models of other physical phenomena). Irrational numbers and complex numbers and quaternions etc. etc. turn out to be good models of other physical phenomena, and other mathematical constructs turn out not to be good models of anything physical but rather just exhibit interesting and useful behavior in their own right (elliptic curves come to mind). None of these things are True. At best they are Useful or Interesting. But all of it is formalizable.

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

#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 branch of mathematics to be developed based on a flawed proof and turn out to be simply false?

Post reply on HN