AI and Math Research

[FactChecker]

@FactChecker i am not saying i am confident about AI being able to explain complicated results all by itself in a future time. i am saying thayt researchers in the AI community will innovate new methods for AI to explain complicated results in a way that is understable to humans. Open AI or any of the big research AI labs has s lot of computational resources to get their own AI systems with guidance from human researchers can find solution to this problems. Put it this way, they have to find it eventually if AI is going to be a scientist that works along side human assisting them in conducting scientific research. It is just a matter of time. As for mathematics, there are the entire catalogue of past issues of American mathematical monthly, Annals of Mathematics and other journals serving as data sets which a capable AI system can train on for writing mathematics well. It is only a matter of priority if large AI research labs choose to spend time on it.

It's a good point that emphasizing explanations of the results may lead to great improvements. I am just a casual amateur and don't know what they are currently doing in the field of AI mathematical proofs.
I will make one observation -- some things are just not simple. I believe that man-made systems are typically designed to make them understandable for humans. Mathematics may be like that. But other things in nature don't care if humans understand and may be overwhelmingly complicated. Examples that come to mind are evolution and DNA; what works, works, no matter how bizarre and complicated it is.

 

[Hornbein]

It's a good point that emphasizing explanations of the results may lead to great improvements. I am just a casual amateur and don't know what they are currently doing in the field of AI mathematical proofs.
I will make one observation -- some things are just not simple. I believe that man-made systems are typically designed to make them understandable for humans. Mathematics may be like that. But other things in nature don't care if humans understand and may be overwhelmingly complicated. Examples that come to mind are evolution and DNA; what works, works, no matter how bazaar and complicated it is.

Having been a student of evolutionary biology my impression is that evolved natural systems tend to be as simple as is possible to get the task done. I find them much more elegant than your typical computer program which is usually a mess. It least it was back then.

 

[Hornbein]

I have heard that automated theorem provers are very picky and demanding and the resulting proofs verbose. That's fine but not something most people would want to deal with.

 

[FactChecker]

Having been a student of evolutionary biology my impression is that evolved natural systems tend to be as simple as is possible to get the task done.

I'll take your word for that. I once tried to go into bioengineering and was blown away by the complexity, but that was just my beginner's impression. I didn't make it far.

I find them much more elegant than your typical computer program which is usually a mess.

Hey!!?? How did you see my computer programs? ;-)

 

[FactChecker]

evolved natural systems tend to be as simple as is possible to get the task done.

I think the key words are "to get the task done". The task includes (as a small part) turning legs back into fins over a millennia when a land animal returns to the water. The task is mind-boggling.

 

[Hornbein]

Terence Tao on human collaboration and computerized proofs. I don't have the patience to listen to it so I just looked at the slides. That's quick. He likes Lean because it facilitates collaboration. Those involved have a common and reliable proof language to share. Then huge proofs can be made.



Kurt Godel proved that there is no lower bound to the required length of minimal proofs.

 

[Hornbein]

"There was a player piano in the home which I found fascinating, though it discouraged me from practicing the piano. As no one had explained to me the nonmechanical aspects of musical performance, I figured that it was a waste of time learning to play the piano when a paper roll with holes in it could do a perfect job.
" Tom Allen in 1930. He did take up the piano when he retired much later.

 

[symbolipoint]

"There was a player piano in the home which I found fascinating, though it discouraged me from practicing the piano. As no one had explained to me the nonmechanical aspects of musical performance, I figured that it was a waste of time learning to play the piano when a paper roll with holes in it could do a perfect job.
" Tom Allen in 1930. He did take up the piano when he retired much later.

Recognize that that represents the restriction on imagination and creativity in piano music and playing. Excellent comparison.

 

[Hornbein]

Recognize that that represents the restriction on imagination and creativity in piano music and playing. Excellent comparison.

A top quality player piano is the best reproduction possible of piano music, better than sound squeezed through microphones. I have heard a piano roll recorded by George Gershwin that sounded quite real. Other such artists are Sergei Rachmaninoff, Sergei Prokofiev, Scott Joplin, Claude Debussy and Maurice Ravel, though I don't know how advanced the technology was in their time.

Today only Bösendorfer makes player pianos, electronic.

 

[FactChecker]

There is one thing I don't think has been mentioned already. No matter how well an AI solution is explained, knowing if the theorem is correct or not can be a big help in arriving at a human understandable proof or counterexample.

 

[Hornbein]

There is one thing I don't think has been mentioned already. No matter how well an AI solution is explained, knowing if the theorem is correct or not can be a big help in arriving at a human understandable proof or counterexample.

Well, knowing that there is a counterexample means that mathers will stop trying to prove it. But the idea is that even failed attempts may come up with something useful as a side effect so discouraging such attempts is bad. Whether that's a good idea or not is beyond me.

This goes all the way back to the computer proof of the four color theorem. It settled the question but didn't lead anywhere. I'm reminded of Hilbert's proof of the Waring conjecture. It was some complicated thing that had no impact on math in general.

I sometimes imagine the Multiverse conference of mathematicians. "So you're from that place where the Riemann hypothesis is true! Purely coincidence. No wonder you have people go crazy trying to prove it. So, what's it like living in a Universe of measure zero?" Response : "All Universes are of measure zero in some way or the other."

"Aha."

 

[FactChecker]

Well, knowing that there is a counterexample means that mathers will stop trying to prove it. But the idea is that even failed attempts may come up with something useful as a side effect so discouraging such attempts is bad. Whether that's a good idea or not is beyond me.

IMO, counterexamples are a very significant part of understanding mathematics.