tech
Brasileiro Leonardo de Moura desenvolve linguagem usada pela OpenAI
Brasileiro Leonardo de Moura desenvolveu a linguagem Lean, utilizada pela OpenAI para solucionar problema matemático do Milênio.
Key points
- A linguagem Lean, criada por Leonardo de Moura em 2013, verifica provas matemáticas para eliminar lacunas e erros lógicos.
- A OpenAI aplicou o Lean para propor a solução do problema de Navier-Stokes, que possui centenas de milhares de linhas de código.
- A IA reduziu para 11 dias um trabalho de formalização do Último Teorema de Fermat que Kevin Buzzard planejava realizar em cinco anos.
Why it matters. A integração de linguagens de verificação como o Lean com a IA pode acelerar a resolução de problemas matemáticos complexos e mudar a prática da disciplina.
O carioca Leonardo de Moura criou a linguagem de programação Lean em 2013 enquanto trabalhava na Microsoft. A OpenAI utilizou a ferramenta em setembro para apresentar uma solução ao problema de Navier-Stokes, um dos Problemas do Milênio com prêmio de US$ 1 milhão. O sistema é usado por matemáticos como Terence Tao e permitiu que Kevin Buzzard formalizasse o Último Teorema de Fermat em 11 dias.
Latest updates
Brasileiro Leonardo de Moura desenvolve linguagem usada pela OpenAI
Criado em 2013 por Leonardo de Moura, o Lean é uma linguagem de programação especializada na verificação de provas matemáticas, eliminando lacunas e erros lógicos. Recentemente, a ferramenta tornou-se central nas operações da OpenAI, empresa responsável pelo ChatGPT, para validar a solução de problemas matemáticos famosos. O sistema permite que argumentos complexos sejam processados passo a passo até a conclusão inevitável. A tecnologia representa um avanço na interseção entre a inteligência artificial e a matemática pura.