Último Teorema de Fermat provado por IA | Lex Fridman

Autoria: Lex Clips · Assistir no YouTube

Vídeo de autoria do canal indicado, não da IANIA; todos os direitos pertencem ao criador. Transcrição, resumo e tradução gerados automaticamente; o conteúdo no idioma original é preservado na versão em idioma original.

Idioma original: inglês

Vídeo original: Fermat’s Last Theorem proved by AI | Lex Fridman · Canal: Lex Clips · 07:55 · Assistir no YouTube

Tópicos: Avaliação e benchmarks de IA, Modelos de IA, Open source e ecossistemas de software

Resumo

O entrevistado conta que a formalização do Último Teorema de Fermat em Lean, com cerca de 13 milhões de linhas, aconteceu muito antes do que ele esperava. Antes disso, acreditava que sistemas de IA conseguiam formalizar textos próximos ao conteúdo da biblioteca Mathlib, mas tinham dificuldade para sintetizar áreas distantes e produzir provas canônicas. A prova foi obtida por sistemas da Anthropic, embora ainda esteja longe da qualidade e da elegância esperadas de uma contribuição integrada à Mathlib. Ele afirma que a autoformalização de teoremas escritos por humanos pode estar resolvida em certo sentido, mas ressalta que construir uma biblioteca matemática clara e útil continuará exigindo muito trabalho humano.

Pontos-chave

A formalização do Último Teorema de Fermat em Lean teria resultado em cerca de 13 milhões de linhas de código.
O entrevistado esperava que esse tipo de resultado ainda estivesse a pelo menos três anos de distância.
Sistemas de IA eram bons em tarefas próximas ao conteúdo existente na Mathlib, mas tinham dificuldade com matemática distante da biblioteca.
A prova foi descrita como sem lacunas marcadas por sorry, mas não como uma prova limpa ou de qualidade Mathlib.
Segundo o entrevistado, a IA combinou e adaptou resultados de maneira pouco canônica, em vez de produzir uma formalização organizada.
A experiência anterior do entrevistado com IA em Lean o levou a esperar melhorias graduais, não um salto dessa magnitude.
Ele acredita que duas ou três pessoas estiveram envolvidas, principalmente incentivando o sistema a continuar, embora ressalve que não conhece todos os detalhes.
A autoformalização de provas escritas por humanos pode estar resolvida em certo sentido, mas aperfeiçoar bibliotecas matemáticas ainda exigirá muito trabalho colaborativo.

Capítulos

Início	Capítulo	Resumo
00:02	O salto inesperado na formalização	O entrevistado compara suas expectativas sobre IA e Lean com a formalização do Último Teorema de Fermat em cerca de 13 milhões de linhas.
02:07	A prova de Fermat em Lean	A conversa aborda as expectativas em torno do projeto e a chegada inesperada de uma prova formal atribuída a sistemas da Anthropic.
03:44	Expectativas e limites das provas geradas por IA	O entrevistado explica por que o resultado superou sua experiência anterior e ressalta que a prova ainda não tem qualidade Mathlib.
05:50	O trabalho humano e o futuro da autoformalização	Os participantes discutem o grau de envolvimento humano, as ressalvas sobre o processo e a continuidade do trabalho para tornar as provas mais organizadas.
07:24	Outros resultados e novas surpresas	O entrevistado comenta que o episódio foi uma nova rodada de surpresa, após ouvir falar de Navier-Stokes e do quasi-RH.

Citações

Tudo o que eu disse naquele colóquio estava errado. — 02:07

Ainda não é uma prova bonita. Não é a prova limpa. — 03:13

Foi completamente além da distribuição do que eu imaginava que esses sistemas eram capazes de fazer. — 05:18

Em termos de obter uma prova sem sorry de algo que seres humanos escreveram no papel, acho que esse problema está resolvido. — 07:24

Conceitos e entidades

Fermat’s Last Theorem (conceito): Teorema cuja formalização em Lean, segundo a conversa, foi produzida por sistemas de IA em uma prova de cerca de 13 milhões de linhas.
Lean (ferramenta): Assistente de provas usado para expressar e verificar formalmente a demonstração discutida.
Mathlib (repo): Biblioteca matemática para Lean, apresentada como referência de organização e qualidade para provas formalizadas.
Anthropic (empresa): Empresa à qual o entrevistado atribui o trabalho dos sistemas de IA que produziram a formalização.
Kevin Buzzard (pessoa): Matemático mencionado por ter recebido uma bolsa para trabalhar na formalização do Último Teorema de Fermat a partir de resultados conhecidos.
Andrew Wiles (pessoa): Matemático citado na referência ao trabalho que levou à prova do Último Teorema de Fermat.
Richard Taylor (pessoa): Matemático citado junto a Andrew Wiles na discussão sobre o trabalho relacionado à prova do teorema.
autoformalização (conceito): Processo de converter matemática escrita por humanos em provas formais verificáveis por um sistema como Lean.
Navier–Stokes equations (conceito): Problema mencionado no encerramento como outro episódio que surpreendeu o entrevistado após o caso de Fermat.

Tradução completa (pt-BR)

00:02 E isso… Este mês tem acontecido um monte de coisas muito além do que eu imaginava ser possível. A formalização do Último Teorema de Fermat: eu tinha certeza de que faltavam pelo menos três anos para conseguirmos fazer algo assim. — Então, talvez você possa falar um pouco mais sobre isso. Foi em Lean, foi formalizado como… Qual era o tamanho do Último Teorema de Fermat em Lean? — Tipo, 13 milhões de linhas. — 13 milhões de linhas. Certo. — Então, eu… Dois dias antes, dei um colóquio no Departamento de Matemática de Princeton, no qual expliquei em detalhes minuciosos o que é Lean, o que é Mathlib, mas também

00:33 que os sistemas de IA de hoje, sabe, têm essa biblioteca Mathlib, onde tudo é feito de forma meio perfeita, exatamente nos níveis certos de generalidade, o suficiente… Não há… Não deveria haver código que reutilize código que esteja demonstrando de novo teoremas em outro lugar. Tudo é o mais geral, o mais abstrato possível, e o que os sistemas de IA conseguem fazer é construir, digamos, uma ou duas camadas em cima disso. Mas o que eles estão fazendo é improvisar de forma meio precária. Ainda não foram treinados para isso — não estou dizendo que não consigam —, mas não são bons nisso agora, no que chamo de canonização, que é

01:05 pegar um código meio desorganizado, refatorá-lo, descobrir exatamente onde ele se encaixa na biblioteca, qual é a versão canônica dessa afirmação, desse lema, e então cada prova deveria ser apenas uma combinação de aplicar este lema daqui, aplicar aquele lema dali, juntar tudo e pronto: aí está o teorema. E então fica tudo bem organizado, bonito, muito elegante. É isso que Mathlib busca. E o que eu disse no meu colóquio foi que, hoje, já é possível formalizar livros didáticos inteiros, desde que estejam no halo de Mathlib.

01:36 Desde que estejam, digamos, a uma, talvez duas etapas de distância de coisas que já foram feitas em Mathlib. Mas, quando você começa — e essa era a minha prática, a minha experiência —, quando começa a pedir que ele faça coisas que estão, sabe, a três ou quatro etapas de distância da biblioteca, a maneira como ele elaborou uma definição para esse objeto e a maneira como elaborou outra definição do mesmo objeto, porque estava fazendo isso com dois propósitos diferentes, entram em conflito. Não dá para juntar essas coisas de novo. Você realmente precisa que a biblioteca, Mathlib, cresça… para chegar a um ponto em que seja possível

02:07 fazer pesquisa em manuscritos que realmente usem e sintetizem várias áreas diferentes da matemática. — Por isso, você esperaria que o Último Teorema de Fermat demorasse bastante: como está tão longe do halo de Mathlib, levaria um bom tempo. — Exatamente. Então, Kevin Buzzard tinha uma bolsa de um milhão de dólares para passar os próximos cinco anos — ou, acho que talvez ele já esteja há um ou dois anos com essa bolsa — reduzindo a formalização do Último Teorema de Fermat a coisas que já eram conhecidas nos anos 1980. Ele queria fazer aquela última etapa, aqueles sete anos de trabalho de Wiles,

02:40 e de Wiles e Taylor, para finalmente concluir, sabe, o Último Teorema de Fermat, mas partindo de coisas que sabíamos que seriam extraordinariamente difíceis. Ele não ia fazer Langlands-Tunnell, não ia fazer Mazur. Havia todo tipo de coisa que se esperava ser ainda muito mais difícil do que aquilo que esses cinco anos exigiriam. E tudo o que eu disse naquele colóquio estava errado. Acho que meu colóquio foi numa quarta-feira. Na sexta-feira, houve o lançamento de 13 milhões de linhas de código a partir dos axiomas: o Último Teorema de Fermat está provado. A afirmação do Último Teorema de Fermat é completamente elementar. Não há alinhamento semântico a

03:13 verificar. Basta dar uma olhada. Sim, essa é a afirmação. Lean diz que ela não tem sorry. — Você pode explicar como foi feito? — Como foi feito? Então, foi a Anthropic, e foi feito porque os sistemas de IA ficaram muito, muito bons em… Ainda não é uma prova bonita. Não é a prova limpa. Ainda há muito trabalho a fazer para transformar essa prova numa prova com a qualidade de Mathlib, e acho que esse é um trabalho importante, que queremos fazer. Mas, para simplesmente obter aquele teorema sem sorry, eles avançaram com força em tudo isso. Improvisaram de forma precária aqui, improvisaram de forma precária ali,

03:44 e, sabe, 13 milhões de linhas depois, tinham uma prova formal de Lean do Último Teorema de Fermat sem sorry. É simplesmente chocante. — A propósito, é sempre bom, hum… Como tudo está avançando tão rápido, vai haver muitas afirmações feitas por todo mundo — por especialistas mundiais — que estarão erradas. Essa é justamente a questão. E o interessante das discussões humanas é que temos discordâncias, e eu arriscaria dizer que algo entre 40% e 80% de tudo o que for dito hoje estará errado daqui a cinco anos, porque tudo está mudando t…

04:16 ão rápido. Mas essa é justamente a questão da discussão, da deliberação e do debate humanos; até mesmo o processo científico consiste em falar bobagem e ver o que se sustenta, com o tempo. Ao longo de dez anos, de cem anos, e assim por diante. — Eu estava descrevendo a minha experiência. Tive muita experiência com Lean e com o uso de IA. Comecei a usar Lean antes de a IA existir no sentido que entendemos hoje, e era um trabalho muito minucioso. E, assim que os sistemas de IA apareceram — sabe, quando os primeiros LLMs começaram a surgir —, eles eram péssimos em

04:47 Lean, mas depois ficaram um pouquinho melhores, um pouquinho melhores, e eu pensei: “Meu Deus, consigo fazer buscas na biblioteca.” Não preciso ficar sentado procurando. Sei que existe um lema que faz isso, mas não sei como se chama, nem exatamente qual é. Está na biblioteca de variedades? Na biblioteca de geometria algébrica? Tipo, me dê este lema, me dê estes lemas. Eles eram ótimos nisso, e eu pensei: “Nossa, isso é incrível. Vou continuar usando esses sistemas.” E toda a minha experiência me dizia que eles conseguiam fazer, tipo, X, mas não 10 X, e isso foi um milhão de X. Estava completamente fora da distribuição do que, na minha cabeça, esses sistemas

05:18 eram capazes de fazer. — Você tem uma estimativa aproximada de quantos humanos estiveram envolvidos nisso e de qual foi o nível de participação humana na geração dessas 13 milhões de linhas de código? — Acredito que foram duas ou três pessoas. — Certo. — E acredito que a maior parte da participação delas foi dizer: “Continuem”, em letras maiúsculas. — Certo. Tudo bem. Então você acha que foi mesmo só uma orientação leve, não algo como criar o caminho e… — Pelo que entendo, não houve conhecimento especializado na área por parte das pessoas que estavam fazendo isso. — Certo.

05:50 — Como diz o meme sobre OpenAI ou Anthropic, sabe, o prompt é “resolva matemática”… ou algo assim. E aí… — Faça uma descoberta revolucionária. — É, é. Isso mesmo. Faça uma descoberta revolucionária. — Faça uma descoberta revolucionária. Esse é o prompt. E aí ele vai lá e faz. — Claro, nunca se sabe. Do ponto de vista de uma empresa, há muitos incentivos para apresentar isso dessa forma, mesmo que talvez tenha havido muitas etapas intermediárias que levaram a isso, em qualquer fase do treinamento, ou talvez algumas coisas tenham ficado sem ser ditas. Mesmo que o prompt final seja “faça uma descoberta revolucionária”, pode ter havido muito

06:23 trabalho preparatório antes disso que levou a esse resultado; não sabemos. — Então, lembro que foi numa sexta-feira porque fiquei completamente… minha cabeça explodiu. E era o Dia do Trabalho, e levamos as crianças à praia, e eu precisava de alguns dias em que, sabe, não olhasse para o celular, não entrasse no Twitter. Só ficava jogando, sabe, jogando meus filhos no oceano e… — Você teve aquele momento em que fica sentado, olhando para o oceano e contemplando? — Sim. Tipo: o que tudo isso significa?

06:53 Então, eu já tinha passado por isso um mês antes. E pensei: eu… Então, o que isso quer dizer agora é que a autoformalização está basicamente resolvida. Não está resolvida do jeito que eu gostaria. Eu quero… E as pessoas ainda vão trabalhar muito, muito duro nisso. Há todo tipo de outras coisas que acontecem, assim como há todo tipo de outras coisas que acontecem quando você prova teoremas, como subprodutos desse processo para a compreensão humana. Há todo tipo de outras coisas quando você trabalha para criar uma biblioteca de matemática bonita, e esse processo vai continuar. Esse processo vai ser

07:24 muito difícil. Vai exigir, sabe, milhares de horas de trabalho de pessoas do mundo todo contribuindo dessa forma open source. Mas, em termos de conseguir uma prova de algo que seres humanos escreveram no papel sem nenhum sorry, acho que esse problema está resolvido. — E então você estava ali, com um uísque, tendo passado por isso um mês antes, e agora de novo. — Isso mesmo. Essa foi a terceira rodada. — Esta é a terceira rodada. — Porque, quando voltei do Labor Day, foi Navier-Stokes. — Navier-Stokes. — Mas este… — Então pensei: “Eu estava acabado de lamentar o FLT. Você vai fazer isso comigo? Qual é?”

07:55 — Mas agora, quero dizer, isso realmente caiu a ficha, não é? Com o quase-RH.

Transcrição original

[00:02] And this is– It’s been a month of things happening way outside of my model of what was possible. The Fermat’s Last Theorem formalization, I was sure we were three years away, at least, from being able to do something like that. - So, maybe you can elaborate on that. It was in Lean, it was formalized as… How big was the Fermat’s Last Theorem in Lean? - Like, 13 million lines. - 13 million lines. Okay. - So I just– Two days before, I gave a colloquium in the Princeton Math Department where I explained in painstaking detail what Lean is, what Mathlib is, but also

[00:33] that AI systems today, you know, there’s this Mathlib library where everything is kind of perfectly done, exactly the right levels of generality, enough– There’s no– There’s not supposed to be any code that’s reusing code that’s reproving theorems somewhere else. Everything is the most general, the most abstract, and what AI systems are capable of doing is building, like, one or two layers on top of that. But they’re, what they’re doing is jerry-rigging. They have not been trained yet, I’m not saying they can’t do it, but they’re not good at it right now, at what I call canonization, which is

[01:05] taking kind of sloppy code, refactoring it, figuring out exactly where in the library it belongs, what’s the canonical version of this statement, of this lemma, and then everything, every proof should just be a combination of you apply this lemma from over here, you apply that lemma from over there, put all these things together, there’s your theorem. And then it’s really clean, it’s really beautiful, very elegant. That’s what Mathlib is going for. And what I said in my colloquium is, where we are today is that you can get entire textbooks formalized as long as they’re in the Mathlib halo.

[01:36] As long as they’re, like, one, maybe two steps removed from things that have already been done in Mathlib. But when you start, and this had been my practice, my experience had been, when you start asking it to do things that are, you know, three or four steps removed from, the library, the way that it came up with a definition of this object and the way that it came up with some other definition of the same object, ’cause it was doing it for two different purposes, then they clash. You can’t stitch these things back together. Like, you really need the library, Mathlib, to grow- … in order to get to a place where you can

[02:07] do research manuscripts, you know that are, that are really using, synthesizing tons of different areas of mathematics. - Which is why you would expect Fermat’s last theorem to take– because it’s so far outside of the halo of Mathlib, it would take quite a bit of time. - Exactly right. So Kevin Buzzard had a million dollar grant to spend the next five years, or I th- maybe he’s already a year or two into that grant, to reduce the formalization of Fermat’s last theorem to things that were known in the 1980s. So he wanted to do that last step, the, those seven years of Wiles’ work,

[02:40] and Wiles Taylor, to finally finish you know, Fermat’s last theorem, but built on top of things that we knew would be extraordinarily difficult. He wasn’t gonna do Langlands’ Tunnell, he wasn’t gonna do Mazur. There were, there were all kinds of things that were expected to be even much more difficult than what these five years would take. And everything I said in that colloquium was wrong. And I think my colloquium was on a Wednesday. On Friday, there was a drop of thirteen million lines of code from the axioms, Fermat’s last theorem is proved. The statement of Fermat’s Last Theorem is completely elementary. There’s no semantic alignment to

[03:13] check. You just glance at it. Yes, that’s the statement. It’s– Lean says it’s sorry-free. - Can you explain how it was done? - How it was done. So it was Anthropic, and how it was done was AI systems just got really, really good at– It’s still not a nice proof. It’s not the clean proof. It’s not– There’s still a ton of work that needs to be done to make that proof a Mathlib quality proof, and I think that’s important work and work that we want to do. But in terms of just getting that sorry-free theorem, they just blasted through all of these. They jerry-rigged this, they jerry-rigged that,

[03:44] and, you know, thirteen million lines later, they had a sorry-free formal Lean proof of Fermat’s Last Theorem. It’s just absolutely shocking. - By the way, it’s beautiful to always, um– Because of how rapid everything is, there’s going to be a lot of statements that everybody makes, the world experts make, that are wrong. That’s the whole point of it. And that’s the fun thing about human discussion, is we have disagreements and I would venture to say somewhere between forty to eighty percent of everything said today will be wrong in five years because everything’s changing s-

[04:16] so fast. But that’s the whole point of human discussion and deliberation and discourse and the, even the scientific process is saying shit and seeing what sticks, Over time. Over ten years, over a hundred years, and so on. - I was describing my experience. I had a lot of experience with Lean and, and with using AI. I started doing Lean before AI existed in the, in the sense that we understand it now, and it was very painstaking. And the second, uh, AI systems came on, you know, the first LLMs were coming online, they were, they were crap at

[04:47] Lean, but then they got a little bit better, a little bit better, and I was like, “Oh my God, I can do library search.” I don’t have to sit there looking, I know there’s a lemma that does this, but I don’t know what it’s called, and I don’t know which exactly. Is it in the manifolds library? Is it in the algebraic geometry library? Like, give me this, give me this lemmas. It was great at that, and I was like, “Oh, this is amazing. I’m gonna keep using these systems.” And every bit of my experience told me that they can do, like, X, but not ten X, and this was a million X. It was just completely outside of the distribution in my mind of what systems

[05:18] were capable of. - Do you have a ballpark estimate of how many humans were involved in that, and, like, what is the level of human involvement in generating those thirteen million lines of code? - Uh, I believe it was two or three humans. - Okay. - And I believe most of their involvement was, “Keep going,” all caps. - Okay. All right, so you think it’s really just, like gentle guidance, not like, you know, pathway creating and- - As far as I understand, there was no domain expertise- - Okay - … on the parts of the people who were doing this.

[05:50] - As the meme goes with OpenAI or Anthropic you know, the prompt is solve math- … or something. And then- - Do a breakthrough. - Yeah, yeah. Yeah, do a breakthrough. - Do a breakthrough. That’s the prompt. And it goes and does it. - Of course, you never know from a company perspective, there’s a lot of incentive to sort of sell it as that, even though there might have been a lot of intermediate steps that led whe- at any stages of the training or maybe some things left unsaid, even though the final prompt is do a breakthrough, there could be a lot

[06:23] of groundwork before that, that led to, we don’t know. - So I remember that was a Friday because I just was completely, like my mind was completely exploded, and it was Labor Day, and we just took the kids to the beach, and I needed a few days of, you know, I’m not checking my phone, I’m not on Twitter. I’m just throwing, you know, throwing my kids into the ocean and, and- - Did you have that moment where you’re just sitting and looking at the ocean and contemplating? - Yeah. Like, what does it all mean?

[06:53] So I had already gone through that a month before. And I was like, I– So now what that says is that autoformalization is basically solved. It’s not solved in the way that I would want it to be solved. I want– And people are still gonna work very, very hard on this. There’s all kinds of other things that happen, just like there’s all kinds of other things that happen when you prove theorems that are byproducts of that process for human understanding. There’s all kinds of other things when you work on making a beautiful library of mathematics, and that process will continue. That process will be

[07:24] very difficult. It’s gonna be the, you know, thousands of man-hours of people around the world contributing in this open source way. But in terms of can you get a sorry-free proof of something that human beings have written down on paper, I think that problem is done. - And so you were standing there with a whiskey, having gone through this a month before, and now again. - Right. This was round three. - This is round three. - ’Cause when I got back from Labor Day, it was Navier-Stokes. - Navier-Stokes. - But this one- - So I was like, “I was just mourning FLT. You’re gonna do this to me? Come on.”

[07:55] - But now, I mean, this really hit home, right? With, with the quasi-RH.