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.
Fermat's Last Theorem – how it’s going
31–40 of 216 posts
Re: Fermat's Last Theorem – how it’s going
#32This 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]
Re: Fermat's Last Theorem – how it’s going
#33Earlier 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".
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
#34This 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.
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
#35I 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: 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…
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.
Re: Fermat's Last Theorem – how it’s going
#38> 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
#39Earlier 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".
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
#40I'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?