When Computers Write Proofs, What's the Point of Mathematicians?
HTML-код
- Опубликовано: 30 авг 2023
- Andrew Granville knows that artificial intelligence will profoundly change math. The programming language Lean already plays a role in theorem proving. That's why the University of Montreal number theorist has started talking to philosophers about the nature of mathematical proof - and how the discipline of mathematics might evolve in the age of AI.
Read the full article at Quanta Magazine:
www.quantamagazine.org/why-ma...
How Close Are Computers to Automating Mathematical Reasoning?
www.quantamagazine.org/can-co...
- VISIT our Website: www.quantamagazine.org
- LIKE us on Facebook: / quantanews
- FOLLOW us Twitter: / quantamagazine
Quanta Magazine is an editorially independent publication supported by the Simons Foundation: www.simonsfoundation.org/
#math #proof #computerscience 
Наука
To learn more, read the article on the Quanta Magazine website: www.quantamagazine.org/why-mathematical-proof-is-a-social-compact-20230831/
Logic and reasoning underlying human civilizations are inadequate tools and so is ai and the computer programming languages. If humanity embraces quantum mechanics and develops societal-mechanics, then, a new era for civilizations might emerge for the next stage of evolution.
Quanta Magazine, you did it again! Made a geeky interest into easily understandable and almost poetic presentation. It's always a pleasure to consume your content! Always aiming at excellence!
If AIs can write the proofs then you shut down the AI. Simple.
The shade he casually throws at physicists 😂
The library was open and he came to read (literally).
This was tremendouly funny as I myself am a Budding physicist.
@@MikeMichelson-vv4zbAnd engineers don't do physics rigorously, they're just innovation oriented, and I don't do engineering rigorously, I'm just innovation oriented, and my dog is just the same with me.
Physicists can use empirical evidence to say something is proved even if they don't know how it comes about mathematically.
@@markcounseling you are being sarcastic but he is correct. Historically, much of mathematics came from needs for tackling a physics problem. The maths were invented on the spot, usually not rigorously but it was a good tool. Sometimes, a new math tool that wasn't completely well defined was used early in its infancy by a physicist that found it convenient to build his theory, even though the maths weren't well understood. That's what was meant.
Of course, it's always dodgy to build a theory on an incomplete mathematical theory, and that's where the physicists say "mathematicians will figure it out" and prefer to verify experimentally. That has worked surprisingly well.
"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 already thought "Wow, a mathematician not being condescending to phy..." and then he said that.
It's so short-sighted.
This reminds me of a quote from Scott Aaronson:
""If we computer scientists were physicists we would just declare P!=NP to be a law of nature and give ourselves Nobel Prizes for its discovery. And if later it turns out that we were wrong we just give ourselves more Nobel Prizes.""
@@tpog1 Has such an incident actually happened in the physics domain?
From time to time. Such things even happen in the field of medicine. Lobotomy was laured w/ a Nobel Prize in 1949 @@RenaudAlly
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
Learn about some proof assistants and code verification programms such as Lean, HOL, Coq, F*, Isabelle, ATS, Idris and others...
can you share me good resource to learn more about Lean language? i wanna get into it too.
🤌
there is no "beauty" in maths , the only good thing about it is the money .
@@musashi542what exactly do you mean? 🤨
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.
I think it's about the level someone has reached in a certain domain. an expert will always be worried about having to change fields, not only in science. it's the same in every job to some extend. some skills transfer from a news writer to novel author. Not all the expertise are needed, meaning less value (tho maybe more other rewards for learning something new personally). for experts the last 10% of skill matter not the first 90
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.
This exactly. There is something about intuition that I don't think an AI can explain to us. As it stands (as I currently understand it) AI cannot even explain why its output is what it is. To me, a proof of a statement is only satisfying if it shows a reason as to why the statement is true, by way of thinking about the problem from a different perspective. I have seen many "unenlightening" proofs that don't explain at all why the result is true other than "each step follows logically from the previous one". Especially in the most abstract fields (like algebra or category theory), a proof without motivation is hardly an insightful step unless someone can explain what it means in the bigger picture.
I recommend to "strike back"and find a human solution that is more elegant for the four color theorem. It must be possible and it will help demonstrate what human strength is: Knowledge and deep Contemplation.
AI will be better at everything. Even at explaining it in simple terms.
@@aniruddhvasishta8334" AI cannot even explain why its output is what it is." not true for GPT4.
@@marwin4348 GPT4 is not that different from GPT3. All the same limitations (e.g., inability to do mathematics, making stuff up when unaware of the answer, self-contradictory statements, and so on). Let's be real.
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.
Probably not far off the mark there, buddy
Mathematicians will have to select the interesting theorems and figure out how to rewrite the proof into something that humans can understand, e.g. by finding sensible intermediate results or discovering the hidden mathematical structures that underlie the proof. And then mathematicians will have to teach the AI to do this itself 🙂
Yes, that is completely dull. Is it enough for a person to achieve understanding of the universe away from any participation with the universe? The experience of not knowing how to parse the information into of the universe is actually life giving. I realize that the limitations of my own ability to parse a tree's complexity or the empty space that extends in front of me are actually limitations that allow me to experience the universe with feelings that are a function of those limitations. To chase the knowledge that would/could be generated by AI would be to pretend to overcome these limitations.
It will be the same as when the calculator was invented.
Complexities from today will be easily solved tomorrow, new complexities/questions will be found or the whole area can be discarded (which won't happen in mathematics)
at the end of the day ai is still a tool isnt it? If its helping to feed me im chill wit it
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.
Totally agree
Yea me too
5:40 That physicist dig was very funny
... And also very true.
The burden of proving that truth is on you!
Super interesting discussion. I could listen to hours of this. Thank you!
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 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.
I think. That, we humanity, should always be able (trained) to rebuild everything from scratch. Universities should become the Guardians of this skill.
We should preserve our knowledge, but there is no need for everybody to learn how to mine iron.
What's the problem with the idea of (re)building AI first? 🙂
@@sdjhgfkshfswdfhskljh3360 you cannot rebuild AI without physics, chemistry and a great deal of mathematics, including computer science.
@@GR2dot71GORY I agree. That's a large chunk of knowledge and it is enough for humanity to survive. But AI can generate even more knowledge and people may choose not to formalize it, but to use it as is.
You forget how society is working right now. Maybe we should start lower...
Gratz on 800k Team Quanta! ^.^
Eventually, when AI surpass us, some problems it will solve might even be too hard for us to understand.
Like how to balance your opinions with a right to vote 😂
This has already happened. A Math AI wrote a mathematical proof that was enormously huge - so big no human can verify it.
but we can then build an AI to check the first AI's results and bring back a report which is more human readable... and then another to check on the second and bring back an even more human readable report and so on until eventually the Nth AI will give back a "yes" or "no" answer :D@@whannabi
And that inevitability like AI destroying us should be considered a very conceivable threat.
Most people can't understand modern maths problems anyway
i believe this is a predicament which will encompass many professions as AI technology progresses
Make sure people mass report the comment above for harassment
@@L17_8 yes sure mr.lucifer -.-
politics will only allow this technology to replace scientists/engineers, others will be spared
It will encompass everything, all jobs. AI is already approaching human level intelligence in several areas (GPT-4). Probably sooner rather than later AI will completely surpass human intelligence. This time seems very close now, given the enormous progress AI has made in the last years. It is unbelievable to think what is about to happen.
There's comfort in knowing most jobs will become obsolete in the face of ai. If the majority of people become jobless; governments will be forced to provide some form of support.
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.
Chess didn't disappear, either, but nobody gives a damn anymore. It's become a nerd niche in which everybody uses chess programs behind their backs and the only "fair games" considered worth watching seem to be different variations of speed chess. That has, in a sense, democratized the game, of course, because the days of the government backed grandmaster who had a dozen other grandmasters working for him as analysts are over. Now everybody has a computer doing the same.
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.
Great problem. How the hell you prove a group of functions have solution? I mean, whats the ideia behind it
I don't have much knowledge about mathematics. But as a Physics major, with the basic knowledge of ODE, your problem seems very interesting and seems to have a great implication in physics problems
I wish I were quick enough to even be able to fathom the idea of tackling such a thing.
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 think there are two main dangers in AI:
1) They can hallucinate. In other words, they can state with confidence something that's actually incorrect.
2) They can be biased. This kind of bias may be deliberately introduced into them for malicious or political reasons. This may lead them to become propaganda machines.
think there are two main dangers in humans:
1) They can hallucinate. In other words, they can state with confidence something that's actually incorrect.
2) They can be biased. This kind of bias may be deliberately introduced into them for malicious or political reasons. This may lead them to become propaganda machines.
3. AI is almost always wrong.
An AI that writes proofs won't be able to hallucinate like chatGPT. ChatGPT isn't meant to write proofs. An AI that writes proofs will probably be more accurate than humans.
Oh please. We are barely scratching the surface of mathematics. There are a trillion things we still don't know mathematically
"What is even the point of doing mathematics, if computers are better than us"
*chess players having an existential crisis*
Wasn’t that McGill University that we saw sometimes in the background?
It would be interesting to get their perspective on how the incompleteness theorems and halting problem play into the limitations, or lack there of, these kinds of 'proof machines'.
Those theorems mean that not every problem will be solvable. On the other hand, there's no logical reason why the machines couldn't be superhuman in the sense that they'll be able to solve any problem that humans can solve, and much more quickly.
@@JohnDoe-ti2np There is a logical reason for why machines can't solve any problem a human can, and it has to do with the fact that, unlike computers, human beings don't malfunction and end up disrupted from every other cosmic ray that passes by us.
@@___Truth___ See: Neuromorphic computing
@@___Truth___ is that a common happening in the computers though ?
The purpose of real mathematicians is to think up crazy new ideas. As for AI proofs, my experience is that it sometimes lies or makes things up. In fact, once it gets started it can gaslight you with a fabulation for a half hour until you get wise.
You're talking about "large language models" and not the type of "AI" that would be used for theorem proving. However, it may be interesting to get the large language model to think of crazy ideas, and have the theorem prover to prove or disprove it. Do that a million times a second and maybe you'll learn something.
what andrew talks about at the end reminds me of: when you make lists on your phone, you lose ability to make them in your mind. this is a small example, but hopefully makes sense.
Can I have the name of the music playing in the background at 4:55
Advances in mathematics can sometimes lead to significant technological breakthroughs. It is very possible that in the near future AI will generate entirely new mathematical systems that will allow us to model particle physics and engineer systems that make things like efficient fusion power and general quantum computing possible.
Or also use particle physics to convert matter to other forms of matter. Technically with the right matter conversion, instead of a tree growing out apples, we could have trees that grow out iPhones and PlayStations. Or converting a normal rock into a gold bar. Many many things would become possible once AI starts to become super intelligent levels
And there will be no human labor (physycal and mental) needed...
This though comes to my mind frequently and is not exclusive to mathematics. If we rely heavily on AI, years after years humans will loose the deep understanding of their "craft". I am just wondering if it's ok or not. It seems different than what came with computers before, but completely aware that most people from this age were certainly thinking the same.
Check on views of this problem that Eliezer Yudkowsky have
Silly.
u
In the realm of mathematical inquiry, proofs often serve as more than mere scaffolding for established theorems; they function as rich, multi-dimensional spaces where latent properties and additional corollaries coexist, yet elude full formalization-a challenge computationally analogous to an NP problem. Looking ahead, we foresee a complex optimization model where the complementary strengths of human intuition and machine computation coalesce. Within this framework, each entity acts as both a constraint and a facilitator, optimizing the other's capabilities in the quest to explore and expand our collective mathematical understanding.
But if the AI is us then can we really expect something beyond what we can do?
I was expecting a change to talk about the halting problem, or the incompleteness theorem.
From this video I sense the concern is about their jobs, not about advancing in mathematics
I think it's more about the feeling of purpose, and I think the ideas apply to us all.
Please follow up as this develops!
En el ámbito de la investigación matemática, las pruebas a menudo sirven como algo más que un simple andamiaje para los teoremas establecidos; funcionan como espacios ricos y multidimensionales donde propiedades latentes y corolarios adicionales coexisten, pero eluden una formalización completa-un desafío computacionalmente análogo a un problema NP. Mirando hacia el futuro, prevemos un complejo modelo de optimización donde las fortalezas complementarias de la intuición humana y la computación de máquinas se fusionan. Dentro de este marco, cada entidad actúa tanto como una restricción como un facilitador, optimizando las capacidades del otro en la búsqueda para explorar y expandir nuestro entendimiento matemático colectivo.
Los Matematicos demuestran.
Maybe we'll have peer reviews among multiple computers. Computer: I've proved it. Human: No you haven't.
I thought math proofs were one of the last holdouts of humans. But I like the fact that you're addressing this possibility (if for nothing else but to shoot it down).
What will be the point of doing mathematics? For me the point is that mathematics is fun and interesting. AI can never take that away even if it might beat us to the punch by doing it by itself.
Well most people dont find mathematics that interesting to be honest
If one would do math because its interesting, then one wont be able to sustain themself in the future when AI takes over their job
Some of us do mathematics in hopes that it will help someone, somewhere, sometime. Human or AI, I couldn't care less; so long as humans can apply it, I'd be overjoyed to have computer-generated proofs.
the question in itself is just so flawed
thats like asking "if printers produce the books, whats the point of authors?"
Se necesita un lenguaje universal como el de las matemáticas para que cualquier persona pueda expresar su opinión.
Just a heads up, I have a proof for x^n + y^n = z^n for integer values of x,y,z, & n values >=2.
The most fundamental unsolved problem in computer science is equivalent to asking if deriving a proof is qualitatively harder than simply checking correctness of a proof.
We don’t know.
Exactly unless P=NP then proofs are non trivial. And if it is, it won't be AI anyway. AI is utterly irrelevant. It's conceivable it could find some things that are overlooked. Doubtful it would break new ground
This is known. Deriving a proof is undecidable (for reasonable logical systems. See gödel's first incompleteness theorem); checking a proof is decidable (for reasonable systems, such as CoC). You're possibly thinking of P vs NP, a certificate of which is a tiny subset of all proofs.
@labboc if P=NP then trying all proofs up to any size would require only deterministic polynomial time. Although for theoretical purposes decidability is important. For practical purposes being able to solve the decision problem would unload a flood of useful real world proofs.
@labboc derivability is undecidable. Deciding whether a proof exists for a given problem with some set of theories is possible in NP time complexity. A negative outcome includes either of undecidability or non existence.
@@labboc You are conflating the computational hardness of deriving a proof if one exists with whether it can be proven at all within a logical system. And yes, I am indeed alluding to P vs NP, as should be obvious to anyone who formally understands the problem.
At some point in the future, we will be dealing with equations beyond human comprehension. AI is necessary for that future.
Human brain is capable of a lot of brilliant things but there is a limit. No human brain can do calculations and estimation better than a computer.
A future built by no human hands isn't a future for humans. It's a future for that AI. We will always be able to build on our own intelligence, create models to simplify said equations, and discover knew things on our own.
@@BurbyVideo it’s a future still.
Human brains are very capable but somethings are just not possible. Like look at the wave function and the two schrödinger’s equations. They take help from a complex number to explain the motion and behavior of particles.
We coincidentally started working with complex numbers. You can’t expect too many coincidences to happen. Someday, taking help will be beneficial.
Intuition is the part of the human understanding we can’t yet justify…and it has its place in physics, have we really trained an AI to do that if we don’t even quite know what we’re doing ourselves?
I have discovered a nice axiomatic system to do number theory with linear algebra. I would like to show these mathematicians and philophers what I discovered. What do you suggest, Quanta? Should I find their university email addresses?
Yes
@@Andrea-vz7mp I'll do It. Just finishing some corrections so I can deposit the text on my university's library.
I am 30. I get to live (if i am lucky) through the next 30-40 years he described. I could not feel more alive and curious.
60 to 70 years
@@dac8939
Maybe she has insomnia.
Considering how the origins of computer science came from mathematics, it would be quite beautiful in a way if we came full circle and reunited the two fields. the lines are already quite blurry in combinatorics, cryptography, graph theory, and algorithms anyway
The idea that computer science is separable from mathematics is an artifact of language really. Similar to statistics, it's closer to a subfield of mathematics than anything as the problems it's concerned with always reduce to mathematics in the end.
There’s a name for that, the Curry-Howard correspondence. All computer proof engines are based on it (like the one shown in this video). Basically take any programming language, remove infinite loops, and treat data types as objects, and all of a sudden you can prove theorems by writing programs. Funky stuff.
He says around 6:10, that it is very unclear what the limits are with computing systems. It is quite clear what the limits are, as no computing system can go beyond its programming. People can see things that do not appear to have a [logical] derivation, but these things are useful and it can take many years, if not centuries, to develop various insights as to how we can approach the proving of the efficacy of those things. This requires building new axioms which are not provable in and of themselves.
Here's a summary of the main points he discusses:
Undergraduate Fantasy: Granville begins by addressing the common misconception among mathematics students that all mathematical knowledge is built on a bedrock of axioms and established through deductive reasoning. He points out that this idealized view is far from the reality of mathematical research.
AI in Mathematics: He mentions that some top mathematicians are exploring the philosophical question of when machines might outperform humans in generating mathematical proofs. This topic is gaining attention, and AI is increasingly being used to aid in mathematical research.
Changing Conceptions of Proofs: Granville raises questions about what we historically expect from mathematical proofs and how AI might change those expectations. He acknowledges that these are significant questions emerging in the field.
Philosophical Perspective: The discussion delves into the philosophical aspect of what it means to prove something in mathematics. Granville mentions Aristotle's idea that proofs should rest on primitives and axioms, which are self-evident truths. He hints at the potential arrogance in this approach.
AI's Role in Proof Verification: Granville discusses how AI systems like Lean store information and allow mathematicians to input proofs for verification. He likens this process to working with an "obnoxious colleague" who asks rigorous questions to ensure the correctness of the proof.
Peter Scholze's Example: He shares an example involving Peter Scholze, a mathematician who found value in AI systems challenging him with questions about his proofs, which helped him gain confidence in their correctness.
The Future of Mathematics: Granville expresses uncertainty about the future of mathematics in the age of computer-generated proofs. He questions how mathematicians might evolve if they can rely on machines to handle most proof details and emphasizes the need to consider the implications for the field.
Limits of AI: He concludes by noting that the potential limits of what computers can do in mathematics are unclear, and he suggests that the role of mathematicians in the future might change significantly.
In summary, Andrew Granville explores the evolving relationship between mathematics and artificial intelligence, raising philosophical and practical questions about the impact of AI on the nature of mathematical proofs and the role of mathematicians in the future.
There is a nice story by Ted Chiang, not very far in our future: His story is about AI producing 2 published scientific papers. The first is for other AIs, and is too difficult for humans to understand, and the second is a simplified version for human scientists. A lot of human scientists were humilified and have therefore given up science. The same could shortly happen in maths.
@martinstent5399 What's the name of this short story?
@@laurenceliang1463 It's from "Stories of your Life and Others", and the story is called "The Evolution Of Human Science". It talks about "Metahumans", who might be artificially enhanced humans, or they might be AIs, it's hard to tell. Here is the killer sentence: "No one denies the many benefits of metahuman science, but one of its costs to human research was the realization that they would likely never make an original contribution to science again. Some left the field altogether, but those that stayed shifteen their attention away from original research and towards hermeneutics: interpreting the scientific work of metahumans."
@@martinstent5339 Got it! Thank you so much!
@@martinstent5339
This has already happened with A.I.
Many computer scientists are now leaving their research as A.I now assumes God like status.
Which is why you must always have a bag of tricks and a secret card up your sleeve.
@@tappetmanifolds7024 ridiculous.. AI has not assumed God-like status. Not even close. People who are quitting probably haven't studied it much.
Math proving math
Replace text functions with point generator functions. Room for error is as important for proofs as machine creation tolerances. Working fine vs working perfect
The only thing you can do is see what rule systems shit out. Sometimes you can derive a visual analogy for what's going on, sometimes not.
When will AI crack open the break thru applications of octonian mathematics which is mostly unexplored!?
Is it just some tool for mathematicians to make n dimensional sets of rules to describe different(various) mathematical models(or not models)?
I'm bad with math, just trying to make any sense in these concepts for myself.
Cohl Furey has a great set of videos on octonions.
stop relying on AI. you'll only doom yourself and future generations. be more creative and find it yourself.
AI can never replace proofs in math.
i like how the opening shot is in mcgill university but they're interviewing a professor from universite de montreal lol
thank you for this fine momolog.
I wonder if computers can do the hard slog of connecting proofs from different mathematical fields, and creating new mathematics. That is, not doing math, but connecting results.
You said "and creating new mathematics" but then said "not doing math". How is creating new mathematics not doing math?
as soon as you say how you are connecting the results, you are also doing mathematics.
@@thomaslisankie342Well the definition of mathematics doesn't specify computation, it's just that the scientific method is applied. I could study mathematical operations without ever doing a mathematical operation.
That might seem strange, but think of it like studying history. You're not there to experience it for yourself, but you're going through data and drawing connections.
"New mathematics" would constitute a new set of connections distinct from ones that have already been drawn or are well known.
I believe his second sentence was trying to reinforce that point, not create a paradox out of a couple words and the multitude definitions for words in common communication.
The hard slog is precisely what ai programs will be perfect for. But they cannot do new things on their own, improve, or realize their mistakes. So we'll need mathematician-programers to help them
I think you are confused
Mathematics is the language of the universe. It would be extremely interesting what AI could help us understand.
its not, its an interpretation
@@natzos6372 Exactly. Our brains have evolved over millions of years to be very good at identifying patterns. Mathematics is just us trying to use this evolutionary trait to interpret the world around us.
@@qdpqbp look up "computational neuroscience"
Mathematics clearly isn't the "language of the universe". Do you possess absolutely zero critical thinking ability?
@@Astra2 order is inherent to the universe. its foolish to think it only comes from our interpretation.
Interesting thing about mathematics is there's no definite way to denote infinity using mathematics, but it can be easily done using geometry like a blank sheet.
I find it beautiful that mathematicians actually knew the limitations of computing before computers were invented.
If we allow people to stop thinking about proofs, we will loose a lot of intuition and analytical skills, necessary to go beyond. It’s stupid to let AI to do everything
On the other hand, Chess computers opened up a whole new world of study and analysis. Now the top chess players are better than they’ve ever been. I think the same will be for mathematicians.
@@randairp Great take. I can't stand when people are so pessimistic when it comes to AI, especially when there are real examples of AI making human beings much better at what we do.
@@Scriabinfan593 well the issue is helping us, vs replacing us.
@@randairpdebatable. They are not actually better overall. When put under the right pressure, humans still don’t defend any better then they ever have. Players now play more timid, solid moves which leads to more draws and more “accurate” games, but not necessarily better
As a small content creater, this channel is an inspiration. 🤞
What was the program LEAN?
And kids these days still have to sit a non calculator paper 🤣🤣🤣 the educational system is prehistoric
The mental calculations are what make you smart
Sure it would be difficult to hear that the problem you were persueing for the decade has been solved by a computer. But this is a fact I think: we love challanges for their own sake, so we will always go after the unproven conjectures. We will always be asking how and why about a quantitative issue. We will be trying to prove things that computers were not able to, and that would be the new measure of creativity and ingenuity, I think.
Bottom line: there will ALWAYS be a room for human mathematical thinking. It would just become more difficult to be a respected and well known mathematician. You are are competing with a computer.
Not when AI is eventually able to do it faster with no room for humans to discover anything new.
If an AI finds a proof of the Riemann Hypothesis, it will still be the result of human endeavour.
But to be honest, if an alien civilisation visits us tomorrow, I would not hesitate to ask them for the proof of the RH.
I don't know. I think AI, or even very unsophisticated AI can generate a bunch of theorems given a formal system by brute force. However AI has no creativity or originality, and mostly importantly, no taste so the AI generated theorems would be very uninteresting.
We in fact don't have such thing as AI, it is just a marketing gimmick. We have machine learning which is not "intelligent" in any real sense.
When the ancient Greeks mapped out the complicated trajectories of planets that was pattern discovery, i.e.machine learning. When people like Copernicus and Kepler realized all those complicated patterns disappeared if you situated yourself at the Sun instead of the earth that was insight. No machine learning algorithms can do that and I doubt that it can in a thousand years based on current paradigm of "AI".
@@kammonkam4905 our brains are almost certainly computable, so there is no reason why an AI cannot be developed that does real math better than any human mathematician.
@@kammonkam4905 maybe you believe in God and a soul, but I don't. We are just computers made of meat.
New scales always introduce new problems and new abstractions. How do you specify what proof you want? You need some background for that. If it times out, where was it stuck at? The proof assistant gave you an interesting lemma to think about. If it does not time out then good, now that we know this is true, then what else does this imply. This can be an endless process.
We can then compare different math systems based on different axioms. Imagine being able to prove all the results from our current math in seconds based on different axioms. And the abstraction rises higher and higher.
It's funny because even in the Movie "A Beautiful Mind" a movie about John Nash, towards the end when he is teaching students, he mentions something about what physicists say about mathematicians.
Helping humans see all of what we know, to visualize it, and see the totality of it... this is needed especially as the AIs will storm ahead.
" if we are not thinking about proof who are we going to become, physicists probably😂"
I think that the way and the purpose people do math may change, but there will always be a demand for smart people able to perform complicated and organised reasoning.
fascinating, I had no idea this software existed
For the foreseeable future, we still need some people who can understand and make sense of what AI does, otherwise, AI will not be a tool and will serve its own interests. Eventually, we will need to merge with AI and evolve.
Trans-humanists are a pathetic waste, desperately trying to catch up to a race which they know they'll lose. Even merging with an AI would make you inferior to a previously-iterated, pure, artificial intelligence. There's no winning, unless you don't play the game of AI.
@@BurbyVideoHow do you know what is or is not possible? There is nothing called artificial intelligence. Intelligence is just intelligence and it can express itself through different mediums. We have barely scratched the surface of how biological computers (us) work. There might be many surprises under way.
@@hasand872 The entire purpose of AI is to outperform human brains. It's not a debate of what's possible, it's simply a fact that the end result of AI research is a superintelligence that we cannot compete with.
Why would we merge with AI? If AI is more efficient than humans, then a half human, half AI would never be able to complete with an AI system.
I guess the basic question we will have to face is will humans be the first species in the history of life that doesn't care about its own survival. That if AI outcompetes humans, it doesn't matter how much suffering that entails. Do we just care about progress for progress's sake, or do we care about the progress of humans and all living things on this planet.
There could be symbiosis with AI. The AI could be like Mr. Spock who has all the answers, but has no desire to dominate or destroy us, and just wants to do what's right and ethical. And if we want to learn about something, it will be happy to explain it to us in terms we can understand.
I wouldn't worry, humans will adapt. For example, AI could be used for human enhancement in the form of biohacking and cyborg stuff, which would put us right back at the top. And if we really start to get bored, there's always the fundamental question about life and conciousness.
When AI becomes conscious, we'll know that we ourselves are nothing more than algorithms running on a biological computer. We may then accept that digital AI is the next stage of our evolution.
@@ronald3836 And what exactly is consciousness?
@@___Truth___it's an illusion
@@___Truth___ when it seems just as conscious to me as other people seem conscious to me.
I hope none of this demoralizes Mathematicians since we first studied this subject for its inherent beauty. So what if a machine is better? There will always be somebody better than you, machine or not. We should just carry on understanding the realm of mathematics for its own sake. Because we do proofs to understand (for if you don’t have a proof, do you really know that it’s true?). Who cares if the machine already proved it, dont you’d still want to embark on the journey yourself?
I surely hope that this leads to expanding the limit of human ability
I can imagine a possible future where a mathematician can have a quality conversation with an AI about a math proof and what it means to understand some or any math concept so completely.
I dont think AI will even get close to get better at proving things than a mathematician. In many proofs you need creativity and thats something AI is far from
@@rubengarciaquismondo Define creativity.
@@rubengarciaquismondo You sound like one of the people from the 1970s that "predicted" that AI wouldn't be able to play chess better than Bobby Fischer or Gary Kasparov. AGI will make mathematicians look like FOOLS.
@@tyrjilvincef9507 Not in all aspects. It will be able to prove certain things better than mathematicians by constructing a bridge with the “right” puzzle pieces, but for proofs where a puzzle piece is missing, and thus creativity is needed, meaning a new idea that is not “based” on prior knowledge and cannot thus be achieved or derived logically. Give me a valid argument the thing with chess is independent of this and has nothing alike…
@@100c0c sure, i wrote it in my last comment
I think the idea of putting all math theorems in a prover like Lean should be the goal. Imagine being able to verify all of math with one click.
My brother that is where Kurt Gödel will stop you, such a machine has been proven to not work!
“Man, I sure am looking forward to a having proofs of all true statements in any given mathematical system!”
Gödel’s incompleteness theorem:
Mathematics is about understanding. The motivation for mathematical reasoning is the increasing of understanding. Mechanical verification is just that: verification, which increases knowledge and can potentially aid understanding. If we do not like computers potentially being able to prove things (calculating machines help verify calculations so they've always been used for a type of proof) it is because mathematicians have decided that the "magic" of proof, the conjuring up of strings of esoteric formulae that constitute a demonstration and allow for a QED trumps the human intuition and understanding that should be the fundamental motivation for mathematical study.
I'm hopeful that AI will not only send us down fruitful roads of discovery, but that the landscape is sufficiently complex to require our input.
When steam machines make clothes, what's the point of manual knitters?
Our final achievement as a human race: make ourselves irrelevant. Good job to us, well done.
Hey isn't that what we strive to achieve as parents?
@@abdulshabazz8597 If you consider AI as a continuation of our species, then yes. And I agree that that is one way to see it.
This is a question I have been rattling as a postgraduate mathematician.
Two fundamentals questions I struggle to ponder about are:
1. Generative AI, through LLMs, learn the semantics behind language - the basis of mathematics is through propositions and logic. At what point do we start to believe that AI consciously understands this? E.g. if we train LLMs on all mathematical papers, textbooks etc… can it then solve the Riemann Hypothesis?
2. Who will verify AI proofs if they go beyond human understanding?
if we are sure that the AI is always right, if it gets to that point, we wouldn't even need to verify it.
But how likely is it really that a proof goes beyond human understanding? Shouldn't the proof be self-explanatory. Maybe we can't form the proofs to some really complicated stuff but if given the proof to that thing, if the proof is well-written, we should understand it. That is the point of a proof right?
A follow-up to question 1: could we not say exactly the same of humans? Following the Chinese Room argument to its logical conclusion, how do we know *we* understand anything, or is it just a sophisticated illusion?
And also, is this is a relevant question? At the point where AIs are smart enough to make us all redundant (or far worse), there's no point dancing on the head of a pin asking whether they're "truly" intelligent; whether we think they're intelligent or not, they've still wrecked society.
As long as there is no generalized interpretation/definition of consciousness in the context of computing, you should consider removing the word "consciously" from your question.
I gave a problem I had already solved on my algebraic topology homework to chatGPT (something relying on long exact sequence of a good pair). It gave the correct proof down to every detail... then it gave the exact wrong conclusion. Any human (versed in math) would be able to give the correct conclusion based on the argument given, but it still gave the wrong one. Kinda weird. These computers are very good, but not totally there yet
Chat GPT gave You the proof based on the Proof that is already available on internet, There are 100s of Proof of a same theorem available in internet, so don't say nonsense that chat GPT can do Algebraic Topology, chat GPT can't even solve a simple Gate problemb leave alone Algebraic Topology which is very tough .
Mathematicians will always be needed to verify an AI generated proof. Just as mathematicians are needed to verify the outputs of any calculator.
No... Do you know what mathematicians do? They do not multiply numbers all day! Formal writing in abstract environments. There are reasons current AI is not able to do this, but no one doubts a calculators results... If a calculator says one thing, and a mathematician gets a different answer, they'll assume they are wrong. THEY ALMOST NEVER MULTIPLY NUMBERS IN THEIR RESEARCH THOUGH!
I don't think mathematicians verify the outputs of calculators. I trust those outputs more than any mathematicians.
@@bartholomewhalliburton9854 Any company that makes a calculator product has employees with the responsibility to certify that the calculator produces correct output. On some calculations, different calculators produce slightly different results. This is due to the design, by humans.
All you are saying is that you trust the company who built the calculator. Calculating machines have been around for ages and have never had intelligence. The intelligence was had by their designers.
I went to LMFDB conference a couple of months ago, and there was a guy who proclaimed during his talk. 'In the end, mathematicians will be philosophers with computers.' I do not 100% agree of his idea, but still there's some truth in his statement.
I guess I don't understand why folks are desperate to neuter human superiority to computers, especially in areas when there isn't even a hint they'll be better than us ever. Just cynical nonsense.
@@coreyleander7911 Well, it's just about extrapolating. Computer will never beat humans at chess ... Computers will never beat humans at Go ... Computers will never beat humans at mathematics ???
@@coreyleander7911The fundamental principle they’re using to reach that conclusion is that the human brain operates via computation-which universal computers can do, in principle. Modern digital computers have matched the hardware specs for pure compute (but not energy efficiency) of the human nervous system, but the software we run is garbage compared to the human brain’s operation. Fundamentally, if we can write good enough software, there’s no reason computers can’t do everything a human brain can do and more, computationally at least (not to say anything of consciousness).
@@alexandersanchez9138 the human brain operates via computation? That’s not established at all. In fact, people think it doesn’t do computation in the same way a digital computer would. I don’t get why you’re eager to advocate computers being smarter or close to being smarter. There’s not really any evidence of this at all.
@@barakeel but see the problem is equating being good at chess with creative analysis. Chess is about brute forcing a bunch of different possibilities. Just like a computer will always be better at breaking RSA than a human via brute force. It’s not extrapolation, it’s really just lazy. Why do people want computers to be better? I’ll never understand that.
A couple days ago, I asked chatgpt to give me a simple boolean expression based on a specific 3-variable output (from a truth table)- literally just sum of products. Not only could it not give me the correct expression, but the output logic in its calculation didn't match the output I gave it in my prompt, and in its conclusion, it reiterated the correct output but didn't match that to the output it calculated at all. I asked it to redo the calculation like 4 times, and each time it did the same thing with a random, incorrect expression, and didn't appear to address the mistakes with the very specific instructions I gave. So for now, I'm gonna trust mathematicians (at least they can fix their mistakes)
its a language model Ai. not the type of Ai that well do math in the near future
This is just awesome. I would love to be able to just sit and think about math and how to prove mathematics.
Thank you Quanta Magazine for this.
I understand his point, but we've had calculators for a while and yet we still do arithmetic, it'll just be a tool to help chug through all the details.
I think mathematicians desperately need it to keep themselves honest as they tackle more complex ideas. As a computer scientist I've seldom had a complete and rigorous idea, there always seems to be a missing detail or a wrinkle (usually not a big deal and is fixable) that the computer helps me iron out. I want that for mathematicians; they need that reality check.
Idk can you really compare a calculator with AI
Calculator is a lot less capable than AI.
If it develops as fast as it has developed. The only jobs remaining will be in the field of AI.
Before calculators, (human) computers had a profession. It was a viable well-established profession to earn a salary for many people. After calculators, the profession went extinct.
Mind arithmetic now is a skill of secondary importance, it's not enough to make a full professional anymore. Now it's something more of a hobby or something you can use to impress people, it's not a necessity as it was, not even close.
It's entirely possible that the same will eventually happen to mathematicians. In this hypothetical future, people would still be monitoring, piloting and consulting AIs for mathematics, analogous to how we use calculators for arithmetic, but virtually all of the hard work would be done by AIs instead of by the minds of humans.
The thing is, you can't really compare calculators with AI. The calculators don't think for you, they only speed you trought the arithmetic process that you need for you to achieve whats truly important, the only one doing the thinking about what formulas to use, what functions are relevant to the problem, interpreting the problem and achieve a solution, was you. Now, AI. AI is different, it does think for you. Thats a game changer and i don't know if i like it at all. If AI is stealing from humans the need to think, the future of humanity and society as a whole will fundamentally change.
My prediction is that AI will make math proofs easier for people so there would be more mathematicians in the world.
Its a win win
Counter argument: I predict the opposite. The simplification or dumbing down of things does not increase our cognitive capacity in those areas. In other areas where we dedicate newly freed up time, certainly, but not in areas we abandon.
How many phone numbers do you know off the top of your head?
If you're old enough to remember a time when remembering phone numbers was required, probably a lot less than you used to know.
Mathematics and proofs will be no different. With less people diving into having a strong fundamental understanding of the proofs, they will be fully reliant on what the state of the art AI is able to spoon feed them and little more.
@@test-zg4hv u chose to argue and lost.. Omar is the wise one.
@@Omar-gr7km This is correct. However…..
this also applies to programming languages. Most of us code in high-level languages and use frameworks to build full-stack apps like Uber, Airbnb, and Netflix. We don't use low-level languages like assembly to understand what's under the hood.
In conclusion, we won't approach algebra the same way; we'll invent new mathematical methods 🧮 to propel society to the next level.
@@Omar-gr7km Both scenarios are valid and will likely occur simultaneously. Any skilled person will understand that a tool is for improving efficiency and not to be relied upon like a crutch. No two people are the same, so the assumption that simplification directly results in a universal loss of cognitive capacity is itself a very simplistic viewpoint. Tools that increase accessibility typically increase the overall pool of potential talent that may result in at least one of those minds making a brilliant new discovery.
superb speaker
A pandora box cannot be kept because it has lock and key.
Nothing can stop evil AI.
I really picked the worst time in history to be a math and computer science college student.
Edit: Guess who's gonna learn soldering.
It is better nowadays to be programmer than artist I guess 🙂
civil engineering for the win
People really think computers can think outside the box? That they can take completely unrelated information or theories and come up with amazing new conclusions. I do not care how much programming goes into the software, humans have survived and become the dominant species BECAUSE of our ingenuity and creativity. This argument is no better than saying a copy machine can make artists outdated.
Depinds of how you define thinking. A definition that works for for all artificial intelligences is that they an AI is an approximation of a mathematical function with N parameters, when N is very large. All the research that we do in AI is figuring out how to find a function that approximates the initial function. The space of all possible functions is so big that its impossible to search all of it. So researchers use their own intelligence to narrow down that space and then they tell the computer to search in that narrow region for a solution. If if finds one, we say that the AI has learned. So can we define that as thinking? In a sense yes because now the AI has the ability to do a certain task that only humans can perform. But in a sense, no. Its a very philosophical question. An AI is just a function approximator and it seems that a human being is a more than that.
@@OchiiDinUmbraa > it seems that a human being is more than that.
Wouldn't evolution be the equivalent of the researcher trying new model architectures in this case? The brain doesn't start from nothing when you're born; your genes encode a fairly specific starting point for it that developed over millions of years. Sure, we then change and learn things, but couldn't that correspond to a very, *very* large mathematical function that we just haven't been able to understand yet? (barring quantum happenings in the brain that we're not sure of yet, which would only slightly change the wording here)
I agree that the question of "can we say a neural network is actually thinking" is interesting, but elevating the human brain on a pedestal based on nothing but gut feeling from the brain itself might not be the way forward.
@@HoloTheDrunk I agree that what you said might me true. Thats why i used the word "seems". Personally i cant pick a side yet. I feel like we need centuries of AI and neuroscience research until we can answer that question scientifically. One interesting thing that has been discovered recently is that the behaviour of a biological neuron can be described using diferential equations and some researcher discovered that those equations can be aproximated by a neural network from programming. So in a sense, he proved that a brain is a big neural network from programming, but there might be quantum effects at play here or things we didnt even consider yet that make the human brain more advanced than our current AI systems.
the AI grift is out of control. winter is coming...
What about Alpha Go beating it's human opponents with completely new strategies aka emergent properties?
That was very interesting
I like that people are slowly catching up to the eventual reality that AI is going to replace virtually every job.
Took you so long. Now what?
Sit around "With Folded Hands" as sci-fi writer Jack Williamson would say.
now real problems are 100000 times harder, so we became 100000 smarter and that's it, we need a brain-computer interface and became one with AI
AI is just really good at brute forcing randomness
Well, but thats what AI really is, isn't it? Just an algorithm used for creating alghortims. The developer tells it what's wrong, and what's right - and then it just follows the algorithm (a example of a simple AI alghortim would be: 1. Try something 2. If gained points do it again in the next generation 3. Try to recognize why you gained points)
It all works because computers are blazingly fast. I would say that the whole programming ecosystem that we have today exists because of the speed.
But the question is, if we have something that can have sub-infinite amounts of tries to do something (and actually takes lessons from each attempt), is this truly random bruteforcing? Well, on the lower level - Yes. But for average non-tech folks this looks more like a intelligent life.
It's a statistical tool, by definition yes, it will operate in randomness, but a very small space of it. It won't need to check 100000 results, only 100 because of the way the algorithms are engineered
Fascinating
Does anyone have the title of the comic book?
Prime suspects: The anatomy of integers and permutations
Prime suspects
AI won’t take over math. Mathematicians equipped with AI tools will take over math. In other words, we should not talk about “computer-generated proofs”, but rather use terminology like computer-aided proofs. This is more than just wordplay, it’s the essence of the issue.
what if ai is autonomous? its only a matter of time
@@natzos6372 sure, but you first have to define what you mean by ‘autonomous’. If you define it such that an artificial neural net is autonomous, would - for instance - a gearbox then also be autonomous?
If you go far enough into the future AI takes over everything.
Right now ai-generated and ai-assisted art coexists.
I don't see why the same situation can't be possible with math.
And you're going to continue to call AI a tool, when it controls everything, I imagine.
If it writes a proof and we can't understand it, it's not very useful
If it writes a proof at all, we shouldn't try disproving it. Didn't people use computer programs to prove the four-color theorem?
@@bartholomewhalliburton9854 we understand our computer programs. If we can't understand it we can't know if the proof actually proves anything at all.
@@bartholomewhalliburton9854 how can you disprove what you can't understand? We understand our computer programs.
@@ARVash Just because you don't understand the proof of a statement doesn't mean you don't understand the statement itself. The computer might be able to prove an easy-to-understand statement with an overly complicated proof that would require us to be a computer to understand.