💻 computer science

ZFLean: a framework for set-level mathematics in Lean

O artigo apresenta o ZFLean, uma biblioteca em Lean 4 que integra a teoria dos conjuntos ZFC central ao ecossistema Mathlib com ergonomia aprimorada, construções canônicas e pontes para tipos nativos, a fim de facilitar provas mistas em nível de conjuntos e tipadas.

Autores originais: Vincent Trélat

Publicado 2026-04-28

📖 5 min de leitura🧠 Leitura aprofundada

CC BY 4.0

Autores originais: Vincent Trélat

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ê está tentando construir uma casa. Você tem dois conjuntos diferentes de plantas e ferramentas:

As Ferramentas "Tipadas" (Sistema Nativo do Lean): Elas são como braços robóticos de alta tecnologia, guiados a laser. São incrivelmente precisos, mas só funcionam se cada tijolo estiver perfeitamente rotulado com seu tipo específico (por exemplo, "Tijolo Vermelho", "Tijolo Azul"). Se você tentar usar um "Tijolo Vermelho" onde um "Tijolo Azul" é exigido, o robô para e se recusa a trabalhar. Isso é ótimo para segurança, mas às vezes a matemática parece precisar ser mais flexível.
As Ferramentas "Conjuntos" (ZFC): Elas são como uma pilha gigante e bagunçada de argila crua. Neste mundo, tudo é apenas "coisa". Você pode moldar um pedaço de argila em uma xícara, uma bola ou um quadrado, e tudo é apenas "argila". É assim que matemáticos tradicionais frequentemente pensam sobre conjuntos: tudo é um elemento de uma coleção, e você pode misturar e combinar livremente.

O Problema:
Por muito tempo, se você quisesse fazer matemática usando as ferramentas "Conjuntos" dentro da oficina de robôs "Tipados", era um pesadelo. Você tinha que constantemente traduzir suas formas de argila em rótulos amigáveis para robôs, provar que sua tradução estava correta e depois traduzir os resultados de volta. Era lento, chato e propenso a erros. A maioria das pessoas simplesmente evitava a pilha de argila por completo e ficava apenas com os robôs.

A Solução: ZFLean
Vincent Trélat criou o ZFLean, que é como construir um tradutor universal e um conjunto de ferramentas personalizadas dentro da própria oficina de robôs.

Veja como funciona, usando analogias simples:

1. A Oficina de "Argila" (O Modelo ZFC)

O ZFLean configura uma zona especial dentro da oficina de robôs onde as regras da "argila" se aplicam. Aqui, você pode definir conjuntos, relações e funções exatamente como um matemático tradicional faria, sem se preocupar com os "tipos" estritos que o robô geralmente exige. É um espaço seguro onde você pode dizer: "Este é um conjunto de números", sem o robô perguntar: "É um Nat ou um Int?"

2. O "Tradutor Inteligente" (O Cálculo Relacional)

A maior dor de cabeça nos velhos tempos era a "burocracia" — a papelada repetitiva e chata necessária para provar que suas formas de argila eram realmente válidas.

O Jeito Antigo: Você tinha que provar manualmente: "Sim, esta relação é uma função" e "Sim, este domínio é válido", para cada passo individual.
O Jeito ZFLean: O framework vem com pequenos assistentes inteligentes (chamados de táticas como zrel, zpfun e zfun). Pense neles como preenchimento automático de formulários. Quando você escreve uma prova, esses assistentes verificam automaticamente os detalhes chatos e preenchem a papelada para você. Você escreve a matemática; os assistentes lidam com o fardo administrativo.

3. A "Ponte" (Interoperabilidade)

Esta é a parte mágica. Geralmente, o mundo da "argila" e o mundo dos "robôs" eram separados. O ZFLean constrói pontes entre eles.

Se você construir um conjunto de números naturais no mundo da argila, o ZFLean pode dizer instantaneamente: "Ei, isso é na verdade o mesmo que o tipo Nat do robô."
Isso significa que você pode fazer sua matemática de teoria dos conjuntos bagunçada e flexível e, em seguida, atravessar a ponte sem problemas para usar as ferramentas poderosas e pré-construídas do robô (como solucionadores de álgebra) para terminar o trabalho. Você não precisa escolher um ou outro; pode usar ambos na mesma prova.

4. O "Kit de Lego" (Construções Canônicas)

Para facilitar a vida, o ZFLean vem com um kit pré-construído de peças padrão de Lego.

Precisa de um conjunto de valores Verdadeiro/Falso? Aqui está um conjunto Booleano.
Precisa de um conjunto de números de contagem? Aqui está um conjunto de Números Naturais.
Precisa de uma maneira de lidar com valores "talvez" (como uma opção)? Aqui está um conjunto Option.
Estes não são apenas argila crua; são pré-moldados, testados e vêm com instruções sobre como usá-los (como "como somar dois números" ou "como inverter um interruptor").

5. O "Test Drive" (O Estudo de Caso)

Para provar que este sistema funciona, o autor o testou com um quebra-cabeça matemático clássico chamado Isomorfismo de Currying.

Imagine isto: Você tem uma máquina que aceita duas entradas ao mesmo tempo (como uma máquina de fazer sanduíches que aceita pão e carne). "Currying" é o processo de transformar isso em uma máquina que aceita uma entrada (pão) e então lhe dá uma nova máquina que aceita a segunda entrada (carne).
O autor usou o ZFLean para provar que essas duas maneiras de pensar sobre a máquina são, na verdade, a mesma coisa. O script de prova parecia quase exatamente como um matemático humano escrevendo-o em um quadro-negro, com os "assistentes inteligentes" lidando silenciosamente com todos os glitches técnicos nos bastidores.

A Conclusão
O ZFLean é um framework que permite aos matemáticos trabalhar no estilo flexível e intuitivo da teoria dos conjuntos tradicional (a "argila") enquanto vivem dentro de um sistema moderno e rigoroso de prova por computador (os "robôs"). Remove o atrito da tradução, automatiza a papelada chata e constrói pontes para que você possa usar as melhores ferramentas de ambos os mundos sem ficar preso no meio.

O resultado é uma biblioteca de cerca de 8.300 linhas de código que faz a matemática em nível de "conjunto" no Lean parecer tão natural e fluida quanto escrevê-la no papel.

1. Formulação do Problema

A formalização moderna em assistentes de prova como o Lean é predominantemente baseada na teoria dos tipos (especificamente teoria dos tipos dependentes), onde objetos matemáticos são tipos construídos. Embora poderosa, essa abordagem pode ser incômoda para a matemática em nível de conjuntos (ZFC), que é frequentemente preferida por:

Raciocínio extensional: Raciocinar sobre igualdade baseada em elementos e não na construção.
Parcialidade: Lidar com funções parciais naturalmente via relações, em vez de codificá-las com tipos Option ou tipos dependentes.
Raciocínio estilo categoria: Trabalhar "a menos de isomorfismo" em vez de igualdade definicional estrita.

O Desafio: Trabalhar diretamente em um modelo teóreo-conjunto dentro de um assistente tipado (como o modelo ZFC do Mathlib do Lean) introduz atrito significativo:

Boilerplate: Os usuários devem gerenciar constantemente "condições laterais" (por exemplo, provar que uma relação é bem-definida, provar que uma função é total) manualmente.
Fragilidade: Cruzar a fronteira entre objetos teóreo-conjuntos (ZFSet) e tipos nativos do Lean (Type) é manual e propenso a erros.
Falta de Automação: Ferramentas existentes frequentemente carecem das dicas de reescrita e táticas específicas necessárias para tornar provas teóreo-conjuntas tão fluidas quanto provas tipadas.

2. Metodologia

O autor apresenta o ZFLean, uma biblioteca Lean 4 construída sobre o modelo ZFC existente do Mathlib. A metodologia foca na criação de um cálculo relacional uniforme e pontes de interoperabilidade para tornar o desenvolvimento em nível de conjuntos ergonômico.

Escolhas de Design Principais:

Fundação: Aproveita a implementação do Mathlib de ZFC, que constrói conjuntos como o quociente extensional de "pré-conjuntos" indutivos (PSet).
Cálculo Relacional: Em vez de tratar funções como objetos totais de primeira classe (como na teoria dos tipos padrão), o ZFLean as trata como relações funcionais. Introduz um cálculo para relações binárias, funções parciais e funções totais.
Automação via Táticas: A estrutura introduz três táticas leves (zrel, zpfun, zfun) projetadas para descarregar automaticamente condições laterais de bem-formação (por exemplo, provar que uma composição é uma relação ou uma função).
Pontes: A biblioteca constrói isomorfismos explícitos (pontes) entre objetos canônicos de ZFC (por exemplo, ZFBool, ZFNat) e tipos nativos do Lean (Bool, Nat), permitindo que propriedades sejam transportadas entre os dois mundos.

3. Contribuições Principais

A. Cálculo Relacional e Automação

Definições: Formaliza inverso, identidade, composição, domínio, imagem e imagem direta para relações.
Funcionalidade: Distingue entre funções parciais (IsPFunc) e funções totais (IsFunc).
Táticas:
- zrel: Descarrega objetivos provando que um conjunto é uma relação ( $R \subseteq A \times B$ ).
- zpfun: Descarrega objetivos provando que um conjunto é uma função parcial.
- zfun: Descarrega objetivos provando que um conjunto é uma função total.
- Essas táticas usam lemas marcados com atributos (por exemplo, @[zfun]) para resolver recursivamente condições laterais, ocultando o boilerplate do usuário.
Notação: Introduz sintaxe conveniente para aplicação de função (@zf(x)) e abstração $\lambda$ , com teoremas para redução $\beta$ , expansão $\eta$ e extensionalidade.

B. Construções Canônicas

A biblioteca fornece um conjunto de objetos matemáticos padrão definidos dentro de ZFC, completos com suas propriedades universais:

Booleanos: Um conjunto de dois elementos $B$ com estrutura algébrica (conjunção, disjunção, negação) e um eliminador de caso.
Números Naturais ( $\mathbb{N}$ ): Definidos como o menor conjunto indutivo (ordinais de von Neumann). Inclui um recursor, princípio de indução e operações aritméticas. Crucialmente, é equipado com uma estrutura CommSemiring para aproveitar a tática ring do Lean.
Inteiros ( $\mathbb{Z}$ ) e Racionais ( $\mathbb{Q}$ ): Construídos como tipos quociente de pares de naturais/inteiros, com operações elevadas a partir de representantes.
Coproductos e Opções: Definições teóreo-conjuntas de tipos soma e tipos opção.

C. Isomorfismos e Transporte

Imersões e Isomorfismos: Define imersões em nível de conjuntos ( $A \hookrightarrow_z B$ ) e isomorfismos ( $A \cong_z B$ ) via funções injetivas e bijetoras.
Teorema de Cantor-Schröder-Bernstein: Formalizado dentro da estrutura.
Transporte: Prova que construções de ZFC são isomórficas aos tipos nativos do Lean (por exemplo, ZFBool $\simeq$ Bool). Isso permite que os usuários "transportem" teoremas da rica biblioteca teóreo-típica do Mathlib para o contexto teóreo-conjunto de forma transparente.

D. Estudo de Caso: Isomorfismo de Currying

O artigo demonstra a utilidade da estrutura provando o Isomorfismo de Currying: $C^{A \times B} \cong (C^B)^A$ .

A prova define curryz e uncurryz como funções em nível de conjuntos.
Prova que são inversos mútuos usando a automação da estrutura para lidar com condições laterais (bem-definição de composições e imagens).
O script de prova espelha de perto argumentos matemáticos padrão, com a camada de automação lidando com a verificação "chata" teóreo-conjunta.

4. Resultados

Tamanho do Artefato: A biblioteca consiste em 8.324 linhas de código Lean e 706 teoremas provados.
Divisão de Componentes:
- Cálculo Relacional: ~2.534 LoC (172 teoremas).
- Naturais: ~1.260 LoC (199 teoremas).
- Imersões/Isomorfismos: ~1.626 LoC (31 teoremas).
Usabilidade: O estudo de caso demonstra que a estrutura reduz com sucesso o atrito da formalização em nível de conjuntos. Os usuários podem escrever provas que se parecem com argumentos teóreo-conjuntos padrão sem provar manualmente que toda composição de relações é uma relação válida.
Interoperabilidade: A capacidade de alternar entre ZFSet e Type nativo permite a reutilização de táticas algébricas do Mathlib (como ring) em objetos teóreo-conjuntos.

5. Significado

Ponte entre Fundamentos: O ZFLean reconcilia efetivamente as visões "teóreo-conjunta" e "teóreo-típica" da matemática dentro de um único assistente de prova. Permite que matemáticos escolham a fundação mais natural para um problema específico (conjuntos extensionais vs. tipos construtivos) sem perder o acesso à automação do ecossistema.
Ergonomia: Ao automatizar as condições laterais tediosas inerentes à teoria dos conjuntos (provas de pertinência, bem-definição de relações), torna o desenvolvimento de ZFC no Lean viável para não especialistas e prático para formalização em grande escala.
Extensibilidade: O design modular (cálculo relacional + objetos canônicos + pontes) permite fácil extensão. Trabalhos futuros incluem a formalização de números reais (via sequências de Cauchy ou cortes de Dedekind) e análise básica.
Comparação: Diferentemente do Isabelle/ZF (onde a teoria dos conjuntos é uma lógica de objeto separada) ou dos desenvolvimentos teóreo-conjuntos do Rocq (que frequentemente carecem de integração profunda com automação teóreo-típica), o ZFLean oferece uma abordagem híbrida que mantém as provas no nível de conjuntos enquanto aproveita a infraestrutura nativa teóreo-típica do Lean.

Em conclusão, o ZFLean fornece uma estrutura robusta, ergonômica e interoperável para fazer matemática fundamental em ZFC dentro do Lean 4, reduzindo com sucesso a barreira de entrada para formalização teóreo-conjunta enquanto mantém compatibilidade com o ecossistema mais amplo do Mathlib.