miniatura|upright=1.7|Uma sessão interativa de prova no RocqIDE, mostrando o roteiro da demonstração à esquerda e o estado da demonstração à direita 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.
Um esforço recente dentro desse campo visa fazer com que essas ferramentas utilizem inteligência artificial para automatizar a formalização da matemática convencional.
Verificação automatizada de demonstrações 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.
História 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.
Comparação de sistemas
Nome Versão mais recente Desenvolvedor(es) Linguagem de implementação Recursos Lógica de ordem superior Tipos dependentes Núcleopequeno Automação de demonstrações Prova porreflexão Geração de código ACL2 8.3 Matt Kaufmann, J Strother Moore Common Lisp Agda 2.8.0 Ulf Norell, Nils Anders Danielsson e Andreas Abel (Chalmers e Gotemburgo) Haskell Albatross 0.4 Helmut Brandl OCaml ainda não implementado F* repositório Microsoft Research e INRIA F* Busca por "proofs by reflection": arXiv:1803.06547 HOL Light repositório John Harrison OCaml HOL4 Kananaskis-13 (ou repositório) Michael Norrish, Konrad Slind e outros Standard ML Idris 2 0.6.0 Edwin Brady Idris Isabelle Isabelle2025 (março de 2025) Larry Paulson (Cambridge), Tobias Nipkow (Munique) e Makarius Wenzel Standard ML, Scala Lean v4.28.0-rc1 Leonardo de Moura (AWS) C++, Lean LEGO 1.3.1 Randy Pollack (Edimburgo) Standard ML Metamath v0.198 Norman Megill ANSI C Mizar 8.1.11 Universidade de Białystok Free Pascal Nqthm NuPRL 5 Universidade Cornell Common Lisp PVS 6.0 SRI International Common Lisp Rocq 9.0 INRIA OCaml Twelf 1.7.1 Frank Pfenning, Carsten Schürmann Standard ML
ACL2 – uma linguagem de programação, uma teoria lógica de primeira ordem e um provador de teoremas (com modos interativo e automático) na tradição de Boyer–Moore. Provadores de teoremas HOL – uma família de ferramentas derivada do provador de teoremas LCF. Nesses sistemas, o núcleo lógico é uma biblioteca de sua linguagem de programação. Os teoremas representam novos elementos da linguagem e só podem ser introduzidos por meio de "estratégias" que garantem a correção lógica. A composição de estratégias fornece aos usuários a capacidade de produzir demonstrações significativas com relativamente poucas interações com o sistema. Os membros da família incluem: HOL4 – o "descendente primário", ainda sob desenvolvimento ativo. Possui suporte para Moscow ML e Poly/ML. Utiliza uma licença de estilo BSD. HOL Light – uma derivação (fork) minimalista de grande difusão, baseada em OCaml. ProofPower – tornou-se proprietário e posteriormente retornou ao código aberto. Baseado em Standard ML. IMPS, An Interactive Mathematical Proof System. Isabelle – é um provador interativo de teoremas no qual outros sistemas podem ser codificados. Isabelle/HOL é a sua instância mais popular, cuja fundamentação é próxima à do provador HOL. Outras instâncias incluem Isabelle/ZF e Isabelle/FOLIsabelle Documentation webpage. Acessado em 22 de abril de 2026: https://isabelle.in.tum.de/documentation.html. A base de código principal é licenciada sob BSD, mas a distribuição do Isabelle reúne diversas ferramentas complementares com licenças diferentes. Jape – baseado em Java. Lean – é tanto um provador interativo de teoremas quanto uma linguagem de programação funcional com tipos dependentes. Baseia-se no cálculo de construções indutivas com universos não cumulativos. A partir da versão 4 (lançada em 2023), é auto-hospedada (self-hosting). Pode ser utilizada para formalizar a matemática (possuindo uma biblioteca ampla e coerente para matemática formal), bem como para verificação de software e de hardware. LEGO Matita – um sistema leve baseado no cálculo de construções indutivas. MINLOG – um assistente de provas baseado em lógica minimal de primeira ordem. Mizar – um assistente de provas baseado em lógica de primeira ordem, no estilo de dedução natural, e na teoria dos conjuntos de Tarski-Grothendieck. PhoX – um assistente de provas extensível baseado em lógica de ordem superior. Prototype Verification System (PVS) – uma linguagem e sistema de provas baseado em lógica de ordem superior. Rocq (anteriormente denominado Coq) – um popular provador interativo de teoremas baseado no cálculo de construções indutivas. Theorem Proving System (TPS) e ETPS – provadores interativos de teoremas também baseados no cálculo lambda simplesmente tipado, mas fundamentados em uma formulação independente da teoria lógica e implementação independente.
Interfaces de usuário 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.
Extensão da formalização 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.
Demonstrações formalizadas notáveis
Abaixo apresenta-se uma lista de demonstrações notáveis formalizadas no âmbito de assistentes de provas:
Teorema Assistente de provas Ano Teorema das quatro cores Rocq 2005 Teorema de Feit-Thompson Rocq 2012 Grupo fundamental da circunferência Rocq 2013 Problema de Erdős–Graham Lean 2022 Conjetura polinomial de Freiman-Ruzsa sobre Lean 2023 BB(5) = 47.176.870 Rocq 2024
Ver também Demonstração automatizada de teoremas Demonstração assistida por computador Verificação formal Prover9 – um provador automatizado de teoremas para lógica de primeira ordem e lógica equacional Manifesto QED Satisfatibilidade módulo teorias Lista de descobertas matemáticas feitas por inteligência artificial
Referências
Bibliografia
Ligações externas Theorem Prover Museum "Introduction" em Certified Programming with Dependent Types (em inglês) Introdução ao assistente de provas Coq (com uma introdução geral à demonstração interativa de teoremas) (em inglês) Demonstração interativa de teoremas para usuários de Agda (em inglês) Lista de ferramentas para demonstração de teoremas (em inglês)
Catálogos Digital Math by Category: Tactic Provers (em inglês) Automated Deduction Systems and Groups (em inglês) Theorem Proving and Automated Reasoning Systems (em inglês) Database of Existing Mechanized Reasoning Systems (em inglês) NuPRL: Other Systems (em inglês) (por Frank Pfenning)
Categoria:Raciocínio automatizado Categoria:Demonstração automatizada de teoremas