A Lean 4 Formalization of Euclidean Domain Algorithms from a 1986 Icon Experimentation Package
Este artigo apresenta uma formalização completa em Lean 4 dos algoritmos do Domínio Euclidiano de 1986 da ICON, separando definições matemáticas, implementações computáveis e reprodução de saídas legadas para fornecer provas verificadas por máquina para procedimentos centrais enquanto preserva os resultados originais do benchmark.
Artigo original sob licença CC BY 4.0 (http://creativecommons.org/licenses/by/4.0/). Esta é uma explicação gerada por IA do artigo abaixo. Não foi escrita nem endossada pelos autores. Para precisão técnica, consulte o artigo original. Ler aviso legal completo
Imagine que você tem um livro de receitas antigo e empoeirado de 1986, escrito por um chef chamado Lars. Este livro contém 14 receitas específicas e complexas para "cozinhar" com números — coisas como encontrar o máximo divisor comum, resolver enigmas com restos ou manipular polinômios. O livro original foi escrito em uma linguagem chamada Icon, que era como uma ferramenta de cozinha especializada e peculiar, que funcionava muito bem na época, mas que agora é difícil para os computadores modernos entenderem.
Este artigo trata de uma equipe que pegou esse livro de receitas de 1986 e o traduziu para Lean 4, uma linguagem moderna e ultra-rigorosa usada para provar verdades matemáticas. Mas eles não apenas traduziram as palavras; eles reconstruíram a cozinha inteira para garantir que a comida tenha exatamente o mesmo sabor, enquanto também adicionaram um "inspetor de segurança" para verificar se a matemática está realmente correta.
Aqui está como eles fizeram isso, dividido em conceitos simples:
1. A Cozinha de Três Andares
O maior desafio foi que as ferramentas matemáticas modernas (chamadas Mathlib) são como uma cozinha de alta tecnologia e automatizada. Elas são perfeitas e comprovadas, mas são "não-computáveis" — ou seja, você não pode realmente executá-las para ver o resultado na tela; elas existem apenas como provas abstratas. O pacote Icon de 1986, no entanto, era um sistema de "executar e ver".
Para unir essa lacuna, os autores construíram uma cozinha com três andares distintos:
- Andar 1: O Andar da Prova (O Inspetor de Segurança). Este andar utiliza as ferramentas matemáticas modernas de alta tecnologia (Mathlib). Ele contém as definições matemáticas do "padrão ouro". Se você perguntar a este andar: "Esta receita está correta?", ele lhe dará um "Sim" verificado por máquina. No entanto, você não pode realizar a culinária real aqui.
- Andar 2: O Andar Computável (A Cozinha de Trabalho). Este é um andar de uma cozinha personalizada, de estilo antigo, que imita exatamente o sistema Icon de 1986. Ele utiliza instruções puras, passo a passo, que um computador pode realmente executar para produzir resultados. Ele ainda não possui o "Inspetor de Segurança", mas produz exatamente os mesmos números do livro original de 1986.
- Andar 3: O Andar do Relatório (O Garçom). Este andar é responsável por formatar a saída. Ele pega os números da Cozinha de Trabalho e os imprime exatamente com a mesma fonte, espaçamento e estilo do relatório de 1986. Isso permite que a equipe faça uma "verificação pontual" para garantir que o novo sistema seja um clone perfeito do antigo.
2. O "Fantasma" na Máquina (A Descoberta do Erro de Digitação)
Uma das partes mais empolgantes do projeto foi um mistério histórico. No relatório de 1986, havia uma tabela de resultados para um cálculo específico (chamado PREM). A tabela impressa mostrava um número enorme e complicado como resposta.
No entanto, quando os autores executaram o código original de 1986 em um computador moderno, a resposta foi zero.
O artigo explica que o relatório de 1986 continha um erro de digitação na tabela impressa. A matemática era, na verdade, simples: dividir um polinômio por uma constante numérica deve sempre deixar um resto de zero. O novo sistema em Lean detectou esse erro ao "cozinhar" a receita e ver que o resultado era zero, não o número gigante impresso no livro. Eles corrigiram um erro de documentação de 40 anos ao executar o código.
3. O Que Eles Realmente Provaram (e o Que Não Provaram)
Os autores são muito honestos sobre o que é "provado" e o que é apenas "confiável".
- As Coisas "Provadas" (Nível A): Para matemática básica de inteiros (como encontrar o máximo divisor comum de dois números inteiros), eles usaram o moderno Inspetor de Segurança. Eles possuem uma garantia verificada por máquina de que esses algoritmos específicos são matematicamente perfeitos.
- As Coisas "Confiáveis" (Nível B): Para as receitas mais complexas e sofisticadas (como divisão de polinômios ou Transformadas Rápidas de Fourier), eles ainda não provaram que estas coincidem com o moderno Inspetor de Segurança. Em vez disso, eles confiam no Teste de Regressão. Isso significa que executaram o novo código e o compararam linha por linha com a saída de 1986. Como o código de 1986 funcionou por 40 anos e o novo código coincide perfeitamente com ele, eles "confiam" nele.
- A Lista de "Tarefas Pendentes" (Nível C): Eles identificaram as "Obrigações de Coerência". Isso é como uma promessa para trabalhos futuros: "Prometemos que eventualmente provaremos que a Cozinha de Trabalho (Andar 2) produz exatamente os mesmos resultados que o Inspetor de Segurança (Andar 1)". Eles ainda não fizeram isso, mas mapearam exatamente onde a prova deve ser aplicada.
4. Por Que Isso Importa
Este artigo não é sobre inventar nova matemática ou usar esses algoritmos para diagnósticos médicos ou viagens espaciais. É sobre preservação e verificação.
- Preservação: Eles salvaram uma parte da história da ciência da computação (o pacote Icon de 1986) ao traduzi-lo para uma linguagem que ainda será legível em 50 anos.
- Verificação: Eles mostraram que até algoritmos "antigos" podem ser rigorosamente verificados. Eles provaram que a lógica de 1986 se sustenta, mesmo que o relatório impresso original tivesse um erro de digitação.
- Transparência: Eles rotularam claramente quais partes do código são matematicamente provadas e quais partes são apenas "nós verificamos contra o livro antigo e coincide".
Em resumo, este artigo é uma renovação de uma cápsula do tempo. Eles pegaram uma casa antiga e levemente empoeirada, reforçaram a fundação com aço moderno (provas em Lean), mantiveram o layout original dos móveis (algoritmos de 1986) e até encontraram uma rachadura na parede (o erro de digitação) que ninguém notou por quatro décadas.
Afogado em artigos na sua área?
Receba digests diários dos artigos mais recentes que correspondam às suas palavras-chave de pesquisa — com resumos técnicos, no seu idioma.