Corrigindo a Prova de Bird para o Crivo de Eratóstenes: Uma Prova sobre Listas Infinitas

Este artigo corrige uma prova errônea de Richard Bird em seu livro *Thinking Functionally with Haskell* sobre o Crivo de Eratóstenes. Bird apresenta uma implementação circular baseada em listas, mas sua dica de prova é falha. Os autores fornecem uma prova de correção completa introduzindo novos lemas e recorrendo a um enfraquecimento do Postulado de Bertrand. A conexão entre este algoritmo e a visão de David Turner de "Programação Funcional Total" também é explorada.