Thanks, John. Very interesting. Mathematicians already add theorems
faster than I can keep up with them. AI will just make me fall further
behind.
Brent
On 6/9/2024 1:08 PM, John Clark wrote:
I've been informed by Brent that the link I gave is behind a paywall.
Sorry about that. Here is the article:
===========
Mathematics is traditionally a solitary science. In 1986 Andrew Wiles
withdrew to his study for seven years to prove Fermat’s theorem. The
resulting proofs are often difficult for colleagues to understand, and
some are still controversial today. But in recent years ever larger
areas of mathematics have been so strictly broken down into their
individual components (“formalized”) that proofs can be checked and
verified by computers.
Terence Tao of the University of California, Los Angeles, is convinced
that these methods open up completely new possibilities for
cooperation in mathematics. And if the latest advances in artificial
intelligence are added to this, completely new ways of working could
be established in the field in the coming years. With the help of
computers, big, unsolved problems could come closer to being solved.
Tao laid out his views on what is to come in an interview with
/Spektrum der Wissenschaft/, /Scientific American/’sGerman-language
sister publication.
[/An edited transcript of the interview follows./]
*In one of your talks at the Joint Mathematics Meetings in San
Francisco, you seemed to suggest that mathematicians don’t trust each
other. What did you mean by that?*
I mean, we do, but you have to know somebody personally. It’s hard to
collaborate with people who you’ve never met unless you can check
their work line by line. Five is kind of a maximum [number of
collaborators], usually.
*With the advent of automated proof checkers, how is this changing?*
Now you can really collaborate with hundreds of people that you’ve
never met before. And you don’t need to trust them, because they
upload code and the Lean compiler
<https://lean-lang.org/about/#:~:text=Lean%20is%20a%20functional%20programming,involves%20defining%20types%20and%20functions.> verifies
it. You can do much larger-scale mathematics than we do normally. When
I formalized our most recent results with what is called the
Polynomial Freiman-Ruzsa (PFR) conjecture, [I was working with] more
than 20 people. We had broken up the proof in lots of little steps,
and each person contributed a proof to one of these little steps. And
I didn’t need to check line by line that the contributions were
correct. I just needed to sort of manage the whole thing and make sure
everything was going in the right direction. It was a different way of
doing mathematics, a more modern way.
*German mathematician and Fields Medalist Peter Scholze collaborated
in a Lean project—even though he told me he doesn’t know much about
computers.*
With these formalization projects, not everyone needs to be a
programmer. Some people can just focus on the mathematical direction;
you’re just splitting up a big mathematical task into lots of smaller
pieces. And then there are people who specialize in turning those
smaller pieces into formal proofs. We don’t need everybody to be a
programmer; we just need some people to be programmers. It’s a
division of labor.
*I heard about machine-assisted proofs 20 years ago, when it was a
very theoretical field. Everybody thought you have to start from
square one—formalize the axioms and then do basic geometry or
algebra—and to get to higher mathematics was beyond people’s
imagination. What has changed that made formal mathematics practical?*
One thing that changed is the development of standard math libraries.
Lean, in particular, has this massive project called mathlib. All the
basic theorems of undergraduate mathematics, such as calculus and
topology, and so forth, have one by one been put in this library. So
people have already put in the work to get from the axioms to a
reasonably high level. And the dream is to actually get [the
libraries] to a graduate level of education. Then it will be much
easier to formalize new fields [of mathematics]. There are also better
ways to search because if you want to prove something, you have to be
able to find the things that it already has confirmed to be true. So
also the development of really smart search engines has been a major
new development.
*So it’s not a question of computing power?*
No, once we had formalized the whole PFR project, it only took like
half an hour to compile it to verify. That’s not the bottleneck—it’s
getting the humans to use it, the usability, the user friendliness.
There’s now a large community of thousands of people, and there’s a
very active online forum to discuss how to make the language better.
*Is Lean the state of the art, or are there competing systems?*
Lean is probably the most active community. For single-author
projects, maybe there are some other languages that are slightly
better, but Lean is easier to pick up in general. And it has a very
nice library and a nice community. It may eventually be replaced by an
alternative, but right now it is the dominant formal language.
*When you gave a talk about a different mathematical project, someone
asked you if you wanted to formalize it, and you basically said that
it takes too long.*
I could formalize it, but it would take a month of my time. Right now
I think we’re not yet at the point where we routinely formalize
everything. You have to pick and choose. You only want to formalize
things that actually do something for you, such as teach you to work
in Lean, or if other people really care about whether this result is
correct or not. But the technology is going to get better. So I think
the smarter thing to do in many cases is just to wait until it’s
easier. Instead of taking 10 times as long to formalize it, it takes
two times as long as the conventional way.
*You even talked about getting that factor down to less than one.*
With AI, there’s a real potential of doing that. I think in the
future, instead of typing up our proofs, we would explain them to some
GPT. And the GPT will try to formalize it in Lean as you go along. If
everything checks out, the GPT will [essentially] say, “Here’s your
paper in LaTeX; here’s your Lean proof. If you like, I can press this
button and submit it to a journal for you.” It could be a wonderful
assistant in the future.
*So far, the idea for the proof still has to come from the human
mathematician, doesn’t it?*
Yes, the fastest way to formalize is to first find the human proof.
Humans come up with the ideas, the first draft of the proof. Then you
convert it to a formal proof. In the future, maybe things will proceed
differently. There could be collaborative projects where we don’t know
how to prove the whole thing. But people have ideas on how to prove
little pieces, and they formalize that and try to put them together.
In the future, I could imagine a big theorem being proven by a
combination of 20 people and a bunch of AIs each proving little
things. And over time, they will get connected, and you can create
some wonderful thing. That will be great. It’ll be many years before
that’s even possible. The technology is not there yet, partly because
formalization is so painful right now.
*I have talked to people that try to use large language models or
similar machine-learning technologies to create new proofs. Tony Wu
and Christian Szegedy, who recently co-founded the company xAI, with
Elon Must and others, told me that in two to three years* *mathematics
will be “solved” in the same sense that chess is solved—that machines
will be better than any human at finding proofs.*
I think in three years AI will become useful for mathematicians. It
will be a great co-pilot. You’re trying to prove a theorem, and
there’s one step that you think is true, but you can’t quite see how
it’s true. And you can say, “AI, can you do this stuff for me?” And it
may say, “I think I can prove this.” I don’t think mathematics will
become solved. If there was another major breakthrough in AI, it’s
possible, but I would say that in three years you will see notable
progress, and it will become more and more manageable to actually use
AI. And even if AI can do the type of mathematics we do now, it means
that we will just move to a higher type of mathematics. So right now,
for example, we prove things one at a time. It’s like individual
craftsmen making a wooden doll or something. You take one doll and you
very carefully paint everything, and so forth, and then you take
another one. The way we do mathematics hasn’t changed that much. But
in every other type of discipline, we have mass production. And so
with AI, we can start proving hundreds of theorems or thousands of
theorems at a time. And human mathematicians will direct the AIs to do
various things. So I think the way we do mathematics will change, but
their time frame is maybe a little bit aggressive.
*I interviewed Peter Scholze when he won the Fields Medal in 2018. I
asked him, How many people understand what you’re doing? And he said
there were about 10 people.*
With formalization projects, what we’ve noticed is that you can
collaborate with people who don’t understand the entire mathematics of
the entire project, but they understand one tiny little piece. It’s
like any modern device. No single person can build a computer on their
own, mine all the metals and refine them, and then create the hardware
and the software. We have all these specialists, and we have a big
logistics supply chain, and eventually we can create a smartphone or
whatever. Right now, in a mathematical collaboration, everyone has to
know pretty much all the mathematics, and that is a stumbling block,
as [Scholze] mentioned. But with these formalizations, it is possible
to compartmentalize and contribute to a project only knowing a piece
of it. I think also we should start formalizing textbooks. If a
textbook is formalized, you can create these very interactive
textbooks, where you could describe the proof of a result in a very
high-level sense, assuming lots of knowledge. But if there are steps
that you don’t understand, you can expand them and go into details—all
the way down the axioms if you want to. No one does this right now for
textbooks because it’s too much work. But if you’re already
formalizing it, the computer can create these interactive textbooks
for you. It will make it easier for a mathematician in one field to
start contributing to another because you can precisely specify
subtasks of a big task that don’t require understanding everything.
*A mathematical proof is not just about checking off that something is
correct. A proof is also about understanding something, right? There
are beautiful proofs, and there are ugly proofs that are very
technical. A good proof gives you a higher understanding of the
matter. So if we delegate that to machines, will we still be able to
understand what they have found out?*
What mathematicians are doing is that we’re exploring the space of
what is true and what is false and why things are true. And the way we
do it is through proofs. Everyone knows that when it’s true, we have
to go try and prove it or disprove it. And that takes a lot of time.
It’s tedious. But in the future, maybe we will just ask an AI, “Is
this true or not?” And we can explore the space much more efficiently,
and we can try to focus on what we actually care about. The AI will
help us a lot by accelerating this process. We will still be driving,
at least for now. Maybe in 50 years things will be different. But in
the near term, AI will automate the boring, trivial stuff first.
*Will AI help us solve the big, unanswered problems in mathematics?*
If you want to prove an unsolved conjecture, one of the first things
you need to do is to break it up into smaller pieces, each of which
has a better chance of being proven. But you will often break up a
problem into harder problems. It’s very easy to transform a problem
into one that’s harder than into one that’s simpler. And AI has not
demonstrated any ability to be any better than humans in this regard.
*By breaking down a problem and exploring it, you learn a lot of new
things on the way, too. Fermat’s Last Theorem, for example, was a
simple conjecture about natural numbers, but the math that was
developed to prove it isn’t necessarily about natural numbers anymore.
So tackling a proof is much more than just proving this one instance.*
Let’s say an AI supplies an incomprehensible, ugly proof. Then you can
work with it, and you can analyze it. Suppose this proof uses 10
hypotheses to get one conclusion—if I delete one hypothesis, does the
proof still work? That’s a science that doesn’t really exist yet
because we don’t have so many AI-generated proofs, but I think there
will be a new type of mathematician that will take AI-generated
mathematics and make it more comprehensible. Like, we have theoretical
and experimental science. There are lots of things that we discover
empirically, but then we do more experiments, and we discover laws of
nature. We don’t do that right now in mathematics. But I think
there’ll be an industry of people trying to extract insight from AI
proofs that initially don’t have any insight.
*So instead of this being the end of mathematics, would it be a bright
future for mathematics?*
I think there’ll be different ways of doing mathematics that just
don’t exist right now. I can see project manager mathematicians who
can organize very complicated projects—they don’t understand all the
mathematics, but they can break things up into smaller pieces and
delegate them to other people, and they have good people skills. Then
there are specialists who work in subfields. There are people who are
good at trying to train AI on specific types of mathematics, and then
there are people who can convert the AI proofs into something
human-readable. It will become much more like the way almost any other
modern industry works. Like, in journalism, not everyone has the same
set of skills. You have editors, you have journalists, and you have
businesspeople, and so forth—we’ll have similar things in mathematics
eventually.
*The math we do is the math that matches our brain, isn’t it? And if
at some point AI is so much smarter, it might go into regions that we
have problems wrapping our mind around.*
Mathematics is already bigger than any one human mind. Mathematicians
routinely rely on results that other people have proven. They kind of
know why it’s true, they have some intuition, but they can’t break it
up all the way down to the axioms. But they know where to look, or
maybe they know someone who can. We already have lots of theorems that
are only verified by a computer, where some massive computer
calculation has checked a million cases. You could verify it by hand,
but no one has the time to do it, and it’s not worth it. So I think we
will adapt. It is not necessary for one person to check everything.
Getting computers to do the checking for us, that’s fine by me.
*At the forefront of math, there’s a lot happening that pulls together
things from seemingly unrelated fields, and from my naive
understanding, an AI that knows all of these fields could give you a
hint and say, “Why don’t you look there? That might help you solve
your problem.”*
It’s a very exciting potential use of AI to create connections or at
least point out possible connections. Right now it has a very lousy
success rate. It might give you 10 suggestions of which one is
interesting and nine are rubbish. It’s actually almost worse than
random. But this could change in the future.
*What are the problems that stand in the way of training a
mathematical AI?*
Part of the problem is that it doesn’t have enough data to train on.
There are published papers online that you can train it on. But I
think a lot of the intuition is not captured in the printed papers in
journals but in conversations with mathematicians, in lectures and in
the way we advise students. Sometimes I joke that what we need to do
is to get GPT to go take a standard graduate education, sit in
graduate classes, ask questions like a student and learn like humans
learn mathematics.
*The published version of a proof is always condensed. And even if you
take all the math that has been published in the history of mankind,
it’s still small compared to what these models are trained on.*
And people only publish the success stories. The data that are really
precious are from when someone tries something, and it doesn’t quite
work, but they know how to fix it. But they only publish the
successful thing, not the process.
*Maybe you should register efforts to prove something, like in medical
studies. The researchers would register it, and then they would have
to publish it even if it didn’t work out.*
We don’t have that culture. Maybe in the future formalization will
become very efficient, and you might be able to formalize things in
real time. And maybe if you want to use some fancy AI Lean of 2040 on
a research project and you want to get funding to use this fancy AI,
you have to agree that your process of trying things and failing is
recorded. And then that could be used to train future AIs. Or maybe
some other group is working on a similar problem, and they can see,
“oh, this other group tried the same thing, but they failed,” so that
you don’t have to waste time making exactly the same mistakes.
*Are mathematicians wasting a lot of time?*
Oh, very much so. So much knowledge is somehow trapped in the head of
individual mathematicians. And only a tiny fraction is made explicit.
But the more we formalize, the more of our implicit knowledge becomes
explicit. So there’ll be unexpected benefits from that.
This article originally appeared in Spektrum der Wissenschaft
<https://www.spektrum.de/news/wie-ki-und-beweispruefer-die-arbeit-von-mathematikern-veraendern/2210083>and
was reproduced with permission.
John K Clark See what's on my new list at Extropolis
<https://groups.google.com/g/extropolis>
rv5
--
You received this message because you are subscribed to the Google
Groups "Everything List" group.
To unsubscribe from this group and stop receiving emails from it, send
an email to everything-list+unsubscr...@googlegroups.com.
To view this discussion on the web visit
https://groups.google.com/d/msgid/everything-list/CAJPayv3SnrNXhEbDHMoC7F-YkikYCfixPGspKkhgN3wsPN1tXg%40mail.gmail.com
<https://groups.google.com/d/msgid/everything-list/CAJPayv3SnrNXhEbDHMoC7F-YkikYCfixPGspKkhgN3wsPN1tXg%40mail.gmail.com?utm_medium=email&utm_source=footer>.
--
You received this message because you are subscribed to the Google Groups
"Everything List" group.
To unsubscribe from this group and stop receiving emails from it, send an email
to everything-list+unsubscr...@googlegroups.com.
To view this discussion on the web visit
https://groups.google.com/d/msgid/everything-list/3d33c5fd-c180-4bb6-a5dd-5591025c7856%40gmail.com.