When Computers Write Proofs, What's the Point of Mathematicians?

To learn more, read the article on the Quanta Magazine website: www.quantamagazine.org/why-mathematical-proof-is-a…

The shade he casually throws at physicists 😂

I am learning math by myself at the moment and I have to say... as someone who hated math in school, now I see the beauty of it because I started learning it in a proof based way. I also learned programming and I feel like the logic of programming and programming languages has helped me gain a new look on math and I'm here for it

"So who are we going to become ? We're going to become more like physicists, probably and say any old nonsense, and just hope the computer verifies it." Savage hahaha

I find it funny that the worst case scenario for a mathematician seems to be to become more like a physicist. The worst case scenario for a physicist usually is becoming an engineer. As a physicist getting more seasoned, I find it sometimes actually refreshing to do something that might be useful during my lifetime. Indeed I am getting old it seems.

The proofs behind mathematical theorems can often carry more weight than the theorems themselves, revealing additional insights that remain a challenge to fully capture. Consequently, the future may see an intricate interdependence between humans and computers, each relying on the other's strengths to advance our collective knowledge.

Imagine that in 10 years from now, AI is so advanced that some AI company comes along and says their new product was able to generate tens of thousands of new mathematical theorems and it keeps generating new ones exponentially based on ones it already proved. What do the mathematicians do then? Just understand and parse through these theorems, and write explanatory textbooks about hundreds of potentially new mathematical fields that just emerged? Life looks really dull when it's just catching up to AI.

Well for us to even understand these proofs we would still need a great deal of familiarity with advanced mathematics and the underlying axioms. Computers could really just help us push the boundaries of mathematical discovery much further by laying down new foundations for understanding deeper theorems yet unsolved or even discovered. I think they could become a real good companion for the mathematician. Its an exciting time to be alive!

I was struck by Andrew’s choice of words and manner of speaking. It shows how well his thoughts converge together and are translated into something remarkable. I have no doubt that years of mathematical experience forces one to transcend into a flow state of ideas.

I think. That, we humanity, should always be able (trained) to rebuild everything from scratch. Universities should become the Guardians of this skill.

I dabbled with COQ. There appeared to be 3 proof methods. 1) rewrites, 2) propositional reasoning, 3) deconstruction of inductive structures, create by induction, then prove by recursion. It seemed in a simple way that a proposition is a long list of symbols, and the proof is a means to strip away the symbols step by step. Also, the approach was very automated so proof would occur without knowing the individual steps sometimes.

Super interesting discussion. I could listen to hours of this. Thank you!

5:40 That physicist dig was very funny ... And also very true.

Gratz on 800k Team Quanta! ^.^

Eventually, when AI surpass us, some problems it will solve might even be too hard for us to understand.

Looking back in history, for example at a big innovation like the computer, I feel confident in saying that although AI will play a bigger and bigger part, it will never be more than a tool. A future mathmatician will be able to expertly navigate this tool to find what he's looking for. Mathmaticians won't disappear, they'll evolve.

i believe this is a predicament which will encompass many professions as AI technology progresses

It's always "i'm scared for us, what about me..." we rarely think bigger than ourselves

This is an interesting thought. I can't but compare the ideas of this video to programming. In an analogy, the numbers and variables in math are much like bits and memory spaces in computer technology repsectivelly. The axioms are the laws of nature that enforce some truths. For example, a bit can be either a one, or a zero, but nothing in between. Or a memory space can only hold up to one bit at a time. Then, upon those truths we start building (in a programming sense, not physically), much like mathematicians. We make programs that handle memory spaces and bits directly, some basic proofs, lets assume. Based on these, we build programming languages that are a bit higher level, just as we do not have to proove that 1 + 1 = 2 anymore. This goes on until we hit a level that is described in this video, which feels like the introduction of frameworks in programming. Based on what we want to build, we use a wide set of tools with complex, ready to go, rarely questioned pieces of code. We achieve things that would be unthinkable to achieve by handling ones and zeroes. We have abstructed so much, that, often, not only do we not know how the bits are behaving, but we do not know how things work several layers higher. And we are not expected to, this would be very hard or even impossible (assuming we advance further). Yet programmers still exist and the things that they produce only get more amazing. They may not be doing the exact same job, but the nature of the job is the same, just like mathematicians may be in the future. Not obsolete, but working to discover even more awesome stuff with the help of powerful tools.

I work in differential algebra. I am trying to prove that all polynomial (algebraic) ODEs can be solved, at least parametrically, via a finite sequence of linear ODEs by introducing new intermediate differential variables. I would love if computer software and hardware technology were at a point where it could help me prove what I want, but currently it's not.