Stanford cria ferramenta de IA que verifica provas matemáticas de artigos científicos em Lean
Investigadores de Stanford apresentaram o PaperFormalizer, sistema que converte artigos científicos em LaTeX num grafo de afirmações e tenta formalizá-las e prová-las na linguagem de verificação formal Lean.
O sistema funciona dentro de um agente de codificação (Claude Code ou Codex), analisando cada afirmação do artigo quanto a fidelidade, ambiguidade e correção antes de tentar formalizá-la em Lean usando a biblioteca Mathlib. Sempre que uma afirmação admite mais de uma leitura, o sistema pausa e pergunta ao autor humano; qualquer correção que altere o que o artigo afirma fica a cargo do autor, nunca automática.
Os autores criaram também um repositório partilhado (paperformalizer.org) onde investigadores podem publicar versões verificadas dos seus artigos. Submetido ao arXiv a 22 de outubro, com código aberto no GitHub.
Perguntas frequentes
O que é Lean?
Uma linguagem de programação e assistente de provas usada para verificar matematicamente que uma afirmação é logicamente correta.
Fontes
- arXiv arxiv.org
- Hugging Face Papers huggingface.co
Resumo editorial em português feito com apoio de inteligência artificial a partir das fontes indicadas. Como fazemos o Boletim IA.