Assistente de provas
Na ciência da computação e na lógica matemática, um assistente de provas ou provador interativo de teoremas é uma ferramenta de software concebida para auxiliar no desenvolvimento de demonstrações formais por meio da colaboração homem-máquina. Isso envolve algum tipo de editor interativo de demonstrações ou outra interface com a qual um ser humano pode guiar a busca por demonstrações, cujos detalhes são armazenados e alguns passos são fornecidos por um computador.
Imagem: Pedro Ribeiro Simões from Lisboa, Portugal · BY · Openverse
A verificação automatizada de demonstrações é o processo de utilizar software para verificar a correção de demonstrações matemáticas. É um dos campos mais desenvolvidos no raciocínio automatizado. A verificação automatizada de demonstrações difere da demonstração automatizada de teoremas porque a verificação automatizada simplesmente checa mecanicamente o funcionamento formal de uma prova existente, em vez de tentar desenvolver novas demonstrações ou teoremas por si mesma. Em decorrência disso, a tarefa de verificação automatizada de provas é muito mais simples do que a de demonstração automatizada de teoremas, permitindo que o software de verificação automatizada seja muito mais simples do que o de demonstração automatizada. Devido a essa dimensão reduzida, alguns sistemas de verificação automatizada de demonstrações podem ter menos de mil linhas de código em seu núcleo (kernel), sendo, portanto, passíveis tanto de verificação manual quanto de verificação formal automatizada de software. O sistema Mizar, o HOL Light e o Metamath são exemplos de sistemas de verificação automatizada de demonstrações. A verificação automatizada pode ser realizada em lote (batch) ou de forma interativa, como parte de um sistema de demonstração interativa de teoremas.
O Automath, desenvolvido por Nicolaas Govert de Bruijn a partir de 1967, é frequentemente considerado o primeiro verificador de demonstrações e o primeiro sistema a utilizar o isomorfismo de Curry-Howard entre programas e demonstrações. O Automath foi utilizado por L.S. van Benthem Jutting em 1977 para formalizar a obra Foundations of Analysis, de Landau, constituindo a primeira formalização dos números reais. Em 1973, Robert S. Boyer e J Strother Moore publicaram Proving Theorems about LISP Functions, cujo objetivo era verificar programas, e não matemática pura. O provador de teoremas desenvolvido por eles é hoje conhecido como ACL2. Na década de 1970, o Edinburgh LCF introduziu a ideia de empregar uma linguagem de programação funcional como metalinguagem para um provador de teoremas, dando origem à família HOL de assistentes de provas. A década de 1990 testemunhou a ascensão do Rocq (então conhecido como Coq), que tem sido utilizado em inúmeros projetos de formalização em larga escala. Desde o final dos anos 2010, o Lean, um assistente de provas fortemente influenciado pelo Rocq, tornou-se outra opção amplamente popular, sobretudo para a formalização da matemática.
Uma interface comumente utilizada para assistentes de provas era o Proof General, baseado no Emacs e desenvolvido na Universidade de Edimburgo. Atualmente, muitos provadores incluem seu próprio editor. O Rocq inclui o RocqIDE, baseado em OCaml/GTK. O Isabelle inclui o Isabelle/jEdit, baseado no jEdit e na infraestrutura Isabelle/Scala para processamento de demonstrações orientadas a documentos. Mais recentemente, extensões para o Visual Studio Code foram desenvolvidas para o Rocq, para o Isabelle por Makarius Wenzel, e para o Lean 4 pelos desenvolvedores do leanprover.
Freek Wiedijk mantém uma classificação de assistentes de provas baseada na quantidade de teoremas formalizados a partir de uma lista de 100 teoremas célebres. Até setembro de 2025, apenas seis sistemas haviam formalizado demonstrações de mais de 70% dos teoremas da lista, a saber: Isabelle, HOL Light, Lean, Rocq, Metamath e Mizar.
Abaixo apresenta-se uma lista de demonstrações notáveis formalizadas no âmbito de assistentes de provas:
