7 ms·
One hour talk, mostly going over the history of machine proofs, and machine assisted proofs. Conclusions (from slides at 49:56) Computers by themselves still
by bagels 3y ago
One hour talk, mostly going over the history of machine proofs, and machine assisted proofs.
Conclusions (from slides at 49:56)
Computers by themselves still seem unlikely to resolve major mathematical problems on their own.
However, they are increasingly being used to generate (sic) assist human mathematicians in a variety of creative ways, beyond just brute-force case checking or computation.
For instance, we have seen they can be useful at generating conjectures or uncovering intriguing mathematical phenomena.
Automated provers could also be used to explore the space of proofs itself, beyond the small set of "human-generatable" proofs that often require one to stay close to other sources of intuition, such as existing literature or connections to other ways of thinking.
While AI technology shows great potential, in the immediate term, I expect it to have the most impact on tasks peripheral to mathematical research rather than central to it, such as automatically summarizing large amounts of literator or suggesting related work.
Proof formalization continues to make steady improvements in speed and ease of use. The "de Brujin factor" (the ratio between the difficulty of writing a correct formal proof and a correct informal proof) is still well above one (I estimate ~ 20), but dropping. Once AI integration takes place, this factor could potentially drop below one, which would be transformative to our field.
- 38 3y ago> However, they are increasingly being used to generate (sic) assist human mathematicians in a variety of creative ways, beyond just brute-force case checking or computation. can you fix this? even with the (sic) I have no idea what you are trying to say here.
- tehnub 3y agoI think it's just that the word "generate" isn't supposed to be there: However, they are increasingly being used to assist human mathematicians in a variety of creative ways, beyond just brute-force case checking or computation.
- bagels 3y agoThat's literally what the slide says. Your guess is as good as mine, and my guess is that there's an extra word, "generate"
- Animats 3y agoProbably. The talk covers many computer-assisted proofs where the big problem was a huge case analysis. The cases have to be generated and machine checked. The proof of the four-color theorem (1,482 cases) was the first major proof like that. It upset many mathematicians.
- senfiaj 3y agoWhy did it upset? Machines are just tools. Is using something beyond a pen and a paper considered a cheating. There are some problems where the easiest way is to just to use brute force. The God's number (the maximum moves to solve the Rubik's cube from any state) was calculated with brute force. If you can formally verify an algorithm I see no problem.
- nicf 3y agoI'm a mathematician, although I'm too young to have been around for this. I feel like I might be able to add a little cultural perspective, though. My impression is that most of the people who were "upset" didn't think that the result was false, or even that the work that went into the Four Color Theorem didn't constitute a proof. It's more that we mathematicians tend to like a proof more when it helps us understand why a fact is true rather than just that a fact is true. So an argument that ends with "and then we checked thousands of cases on a computer and it turned out they all worked" feels unsatisfying, since it feels like it doesn't fully explain what's going on.
- baq 3y agohttps://en.wikipedia.org/wiki/Sic https://en.wikipedia.org/wiki/Sic > in full: sic erat scriptum, "thus was it written"