Quando computadores escrevem ou descobrem provas matemáticas, qual é a função do matemático? Essa questão levantada pelo advento da inteligência artificial está colocando em xeque tudo o que se sabe sobre o trabalho do matemático nos dias atuais e no futuro próximo.

When Computers Write Proofs, What’s the Point of Mathematicians? | Quanta Magazine
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.

Tradução:

Andrew Granville sabe que a inteligência artificial mudará profundamente a matemática. A linguagem de programação Lean já desempenha um papel na prova de teoremas. É por isso que o teórico dos números da Universidade de Montreal começou a conversar com filósofos sobre a natureza da prova matemática – e como a disciplina da matemática pode evoluir na era da Inteligência Artificial.

Quando os estudantes vão para a universidade para estudar matemática, o calouro fantasia que ensinamos que temos esta base sólida de axiomas e tudo é construído sobre esses axiomas unicamente através do argumento dedutivo, e que temos um edifício imponente de matemática brilhante, tudo isso solidamente estabelecido de forma incontestável. É um belo tipo de concepção; o problema é que isso não é verdade. Não está nem perto da verdade. É quase impossível viver de acordo com essa fantasia.

Alguns dos principais matemáticos do mundo têm encarado isto como uma questão de filosofia; na verdade, tenho trabalhado com IA. Se você começar sempre a inserir suas idéias ou provas em uma máquina, em que ponto a máquina fará um trabalho melhor para ajudar a adivinhar o próximo passo? Obviamente isso é um assunto muito quente agora. A situação está avançando rapidamente e a questão é: bem, o que queremos das provas? Historicamente, o que precisamos das provas? Em que acreditamos quando algo é provado e como a IA muda isso? Essas são questões enormes que estão saindo da toca agora.

Meu nome é Andrew Granville; Eu trabalho com teoria analítica dos números. Quando eu era jovem, trabalhei no Último Teorema de Fermat antes de ele ser provado. Hoje trabalho com idéias de funções L e funções multiplicativas. Mas estou interessado em todos os diferentes aspectos, incluindo questões computacionais e algorítmicas. Há muito tempo estou interessado na escrita popular em matemática. Minha irmã é escritora. Estávamos pensando que seria divertido fazer uma história em quadrinhos em matemática, então trabalhamos juntos para desenvolvê-la e eventualmente a escrevemos. Na história em quadrinhos, senti que havia espaço para desenvolvermos filosofia.

Um filósofo da matemática, Michael Hallett, a leu e ficou muito interessado na forma como retratamos a matemática sendo feita. “Você não pode prová-las porque não pode voltar a nada mais primitivo do que essas próprias proposições; elas não precisam de justificativa.” Conversando com Michael, percebi que há um debate sobre o que queremos dizer quando afirmamos que algo foi provado. “Então Aristóteles disse que para provar que algo é verdadeiro, para estabelecer que é verdade, o seu argumento deve basear-se no que ele chamou de primitivos, coisas que você já sabia que eram verdadeiras.” E eventualmente deve haver alguns átomos ali, os chamados axiomas nos quais você baseia todos os seus argumentos. As coisas básicas que você não pode definir, como ponto, linha, plano, se você está falando sobre geometria; você não pode defini-las. Em vez disso, o que você faz é estabelecer alguns axiomas sobre elas. A frase que me vem à mente é que essas verdades são evidentes. Hum, o que, você sabe, é interessante em muitos níveis quando comparado com a matemática. Quer dizer, há uma certa arrogância nisso.

A forma como isso tem sido feito tradicionalmente é que publicamos artigos e há artigos que são colocados em revistas ou livros, e esses livros são colocados em bibliotecas. E então quando queríamos verificar uma verdade, íamos à biblioteca e conferimos o livro e víamos se estava exatamente como queríamos. Isso nos ajudaria a obter uma nova compreensão, ou teríamos que revisar o que estava naqueles livros. Hoje, a inteligência artificial usada como prova de que está fazendo algo semelhante, exceto que vai armazenar essas informações dentro do programa. Então programas como o Lean possuem uma biblioteca de coisas já comprovadas com base em axiomas e depois com trabalho adequado, e é complicado, um matemático pode inserir sua prova no Lean e verificar todos os passos da lógica, pelo menos de acordo com o Lean.

Então, o que o Lean faz? Acho que tenho uma prova de um teorema e quero uma prova formal. Escrevi algo sobre o qual estou um pouco duvidoso. Não quero entrar em todos os detalhes dos prós e contras do conhecimento, pois quando você volta para a Árvore do Conhecimento, tudo realmente vai funcionar. Então a idéia é inserir isso no Lean. Ele age como um colega desagradável que simplesmente não desiste. Se ele não entende, não deixará de importuná-lo com perguntas irritantes. Mas às vezes esse colega realmente ajuda você porque, ao explicar isso a ele, você percebe: “Ah, sim. Ah, é mais simples do que eu pensava.”. Este é um exemplo particularmente famoso de Peter Scholze. Ele tinha uma prova muito, muito difícil da qual não tinha 100% de certeza. Ele tentava dizer, bem, isso é verdade e você deveria saber disso Lean e Lean diria, eu não sabia disso de jeito nenhum. Você vai ter que explicar isso melhor. As partes em que ele se sentiu desconfortável com o que escreveu foram onde mais perguntas foram feitas. Então ele se sentiu bem, isso foi uma verificação e foi fazer as perguntas certas de maneira sensata. Então é um momento emocionante.

A questão é: as máquinas mudarão a matemática? Como você faz com que os computadores o conduzam em uma prova, não apenas o sigam ou façam sugestões, mas provem as próprias coisas? Isto é algo que está ainda na sua infância; muito do trabalho em provas geradas por computador até agora não teve muitas conseqüências. Muito interessante por si só, mas não no quadro geral. Mas existem algumas idéias novas muito interessantes e entusiasmantes. Qual delas tem algum otimismo de que possamos ver o início da geração de novas provas interessantes?

E aí isso começa a ficar um pouco assustador, quer dizer, a gente valoriza a nossa profissão. Valorizamos nosso trabalho pela profundidade das provas. Mas se podemos contar com uma máquina para acertar todos os detalhes, bem, a maioria dos detalhes, então quem somos nós? Qual é a nossa formação? O que é que valorizamos? Então, quando não precisamos pensar em provas, não seremos treinados para pensar em provas. Então, quem vamos nos tornar? Provavelmente nos tornaremos mais como físicos e diremos qualquer bobagem antiga, e apenas esperamos que o computador verifique isso. Acho que é muito difícil prever qual será o sentido de fazer matemática daqui a 30 ou 40 anos. A idéia de provas geradas por computador apresenta novas possibilidades. Com o tempo, vemos, é claro, cada vez mais coisas que os computadores são capazes de fazer, e não está claro quais são os limites.

Transcrição:

When students go to university to study mathematics, the undergraduate fantasy that we teach is that we have this bedrock of axioms and everything is built solely on these axioms through deductive argument, and that we have a towering edifice of brilliant mathematics, all of which is solidly established in an incontrovertible way. It’s a beautiful kind of conception; the problem is that’s not true. It’s not even close to the truth. It’s almost impossible to live up to that fantasy.

Some of the top mathematicians in the world have been looking at this as a philosophy question; I’ve been actually working with A.I. If you start always inputting your ideas or proofs into a machine, at what point does the machine do a better job of helping guess the next step? Obviously this is something very hot right now. It’s moving fast and the question becomes, well, what is it we want from proofs? What have we historically needed from proofs? What is it we believe when something’s proved and how does AI change that? These are massive questions that that are popping out of the woodwork right now.

I’m Andrew Granville; I work in analytic number theory. When I was young, I worked on Fermat’s Last Theorem before it was proved. Today, I work in ideas of L functions and multiplicative functions. But I’m interested in all different aspects, including computational and algorithmic questions. I’ve long been interested in popular writing in mathematics. My sister is a writer. We’ve been thinking it would be fun to do a graphic novel in mathematics, so we worked together to develop it and eventually wrote it. In the graphic novel, I felt like there was room for us to develop philosophy.

A philosopher of mathematics, Michael Hallett, read it and he was very interested in the way we portrayed mathematics being done. You cannot prove them because you cannot go back to anything more primitive than those propositions themselves; they are not in need of justification. Talking to Michael, I realized there is this debate of what it is we mean when we say we’ve got something proved. So Aristotle said that to prove something is true, to establish it’s true, your argument should rest on what he called primitives, things you already knew to be true. And eventually there’s got to be some atoms there, the so-called axioms that you rest all your arguments on. The basic things you cannot define, so like point, line, plane, if you’re talking about geometry, you can’t define those. What you do instead is lay down some axioms about them. The phrase that comes to my mind is these truths are self-evident. Um, which, you know, is interesting at many levels when you compare it to mathematics. I mean, there’s a certain arrogance about it.

The way it’s traditionally been done is that we publish papers and there’s papers that put in journals or books, and those books are put in libraries. And then when we wanted to verify a truth, we go to the library and we check out the book and we’d see if it was exactly as we wanted it. It would help us gain new understanding, or we’d have to revise what was in those books. Today, The artificial intelligence that is used for proof they’re doing something similar, except they’re going to store that information within the program. So programs like Lean have a library of things already proven based on axioms and then with suitable work, and it’s complicated, a mathematician can input their proof into Lean and verify all the steps of logical, at least according to Lean.

So what does Lean do? I think I have a proof of a theorem and I want a formal proof. I’ve written something that I am a bit iffy about. I don’t want to get into all of the details of the ins and outs of know, as you sort of go back to the Tree of Knowledge, everything’s really going to work. So the idea is to input that into Lean. It acts like an obnoxious colleague who just won’t let go. If they don’t understand, they will not stop pestering you with annoying questions. But sometimes those colleagues actually help you because by explaining it to them you realize, Oh yeah. Oh, it’s simpler than I thought. This is particularly famous example by Peter Scholze. He had a very, very difficult proof that he wasn’t 100% sure of. He would try and say, well, this is true and you should know this Lean and Lean would say, I didn’t know this at all. You’re going to have to explain this better. The bits where he had been uncomfortable with what he’d written, it was where it asked the most questions. So he felt okay, that was verification and it was sensibly asking the right questions. So it’s an exciting time.

The question is: will machines change mathematics? How do you get computers to lead you in a proof, not just follow you or make suggestions, but prove things itself? This is something in its infancy; a lot of the work on computer generated proofs up to now has not done much of consequence. Very interesting within itself, but not in the bigger picture. But there are some very interesting, exciting new ideas, which one has some optimism that we may see the start of generating interesting new proofs?

And so this starts to become a little frightening, I mean, we value our profession. We value our work by the profundity of proofs. But if we can rely on a machine to get all the details right, well, most of the details right, then who are we? What is our training? What is it that we value? So when we don’t need to think about proof, then we’re not going to be trained in thinking about proof. 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. I think it’s very hard to predict what even will be the point of doing mathematics in 30 or 40 years’ time. The idea of computer generated proofs these present new possibilities. Over time, we see, of course, more and more things that computers are able to do, and it’s very unclear what limits there are.