PaperFormalizer transforma artigos em LaTeX em código Lean verificado, com participação do autor

Uma equipe de Stanford propôs um método que pretende tornar a verificação formal de artigos de matemática uma etapa rotineira da preparação de uma publicação. O PaperFormalizer, lançado por Jiyuan Tan, Vasilis Syrgkanis e Jose Blanchet, converte o código-fonte LaTeX em uma versão do trabalho verificada pelo Lean. Ele funciona como um pipeline agêntico dentro do Claude Code ou do Codex. A ideia central: mesmo um artigo revisado com cuidado pode conter pequenas lacunas nas provas ou na formulação das hipóteses, e quem melhor as corrige é o próprio autor, com a ajuda da máquina.

Do LaTeX ao Lean: como funciona o pipeline

O processo começa pelo código-fonte. O PaperFormalizer transcreve o artigo em um grafo de dependências entre enunciados: quais lemas são necessários para cada teorema e o que se apoia em quê. Em seguida, cada enunciado passa por uma auditoria em linguagem natural em três eixos: fidelidade ao sentido original, ambiguidade e correção. Só depois disso o sistema formaliza os enunciados e os prova em Lean.

Para as provas, o pipeline recorre a várias fontes:

• Mathlib, a principal biblioteca matemática do Lean;
• bibliotecas de domínio opcionais, voltadas a uma área específica;
• o conjunto de ferramentas pessoal do autor, ou seja, seus próprios lemas e definições.

Esse conjunto é cumulativo. Quanto mais artigos o autor passa pelo sistema, mais blocos prontos ficam disponíveis para o seguinte.

O autor decide o que o artigo afirma

A autoformalização costuma sofrer com a troca silenciosa de significado. Um modelo pode provar um teorema formalmente impecável que diz algo diferente do que o autor tinha em mente. Os criadores do PaperFormalizer partem do princípio de que só o autor sabe o que um enunciado deve significar e qual é a melhor maneira de fechar uma lacuna de formalização.

Por isso, o sistema segue algumas regras:

• se um enunciado admite mais de uma leitura, o pipeline para e faz uma pergunta;
• cada correção é apresentada em linguagem natural e em símbolos TeX como uma sugestão que o autor pode aceitar, recusar ou redirecionar;
• qualquer decisão capaz de alterar o que o artigo afirma fica a cargo do autor.

Diferentemente de sistemas que tentam formalizar trabalhos alheios de forma inteira e autônoma, aqui o humano é o árbitro do significado, e a máquina assume a parte pesada da mecânica das provas.

O que o autor recebe no final

O resultado tem três partes:

• uma versão anotada e corrigida do artigo;
• um relatório com todas as alterações feitas;
• o código Lean, em que cada declaração está ligada ao enunciado que ela formaliza.

Essa última ligação é importante para o leitor. Dá para abrir qualquer teorema do texto e ver o objeto Lean verificado correspondente, sem precisar procurar a correspondência manualmente.

Uma biblioteca compartilhada de trabalhos verificados

Os autores propõem também uma camada de ecossistema. Pesquisadores podem publicar artigos verificados no site paperformalizer.org, e quem constrói sobre esses resultados pode reaproveitar o código Lean já pronto. Isso reduz o custo de formalizar o trabalho seguinte na mesma área: as definições e os lemas necessários já existem e estão verificados.

A ferramenta está publicada no GitHub, no repositório Jiyuan-Tan/PaperFormalizer. O trabalho saiu em 22 de outubro de 2026 e entrou na seleção diária do Hugging Face Papers; a página indica a organização como Stanford University.

Que utilidade tem para pesquisadores

Para matemáticos e teóricos de estatística, economia e aprendizado de máquina, cujas conclusões dependem de provas, é uma forma de obter uma verificação independente antes de enviar o artigo a um periódico. É especialmente útil onde erros nas hipóteses passam despercebidos pela revisão por pares. A barreira de entrada é menor que a da formalização manual em Lean: bastam o código-fonte LaTeX, acesso ao Claude Code ou ao Codex e disposição para responder às perguntas do sistema.

Também é preciso cautela. O pipeline verifica que o enunciado formal foi provado, mas a conformidade da formalização com a intenção original continua sendo confirmada por um humano. Por isso, a qualidade do resultado depende da atenção do autor justamente nos pontos em que o sistema para e faz perguntas.