Resumo Técnico: Formalizando Álgebras de Bandeiras em Lean

Declaração do Problema

A teoria extremal de grafos frequentemente aborda questões relativas à frequência máxima de um padrão finito específico $F$ em grafos que evitam um conjunto de padrões proibidos $H$. Determinar a densidade de Turán assintótica $\pi(F; H)$ é notoriamente difícil porque requer o controle do comportamento de todos os grafos livres de $H$ suficientemente grandes. O método da álgebra de bandeiras (flag algebra) de Razborov fornece uma técnica poderosa para este cenário, reduzindo a prova de limites assintóticos à verificação de um número finito de condições algébricas via programação semidefinida (SDP).

No entanto, a aplicação prática deste método depende de "certificados candidatos" gerados por solvers de SDP externos (por exemplo, Flagmatic). Estes certificados consistem em milhares de valores de densidade exatos e matrizes racionais semidefinidas positivas (PSD). Embora matematicamente sólidos, a verificação destes certificados à mão é impraticável, e confiar em software externo sem verificação formal introduz uma lacuna na cadeia lógica da prova. O desafio é criar um framework verificável por máquina que possa ingerir estes certificados externos, verificar os dados combinatórios finitos subjacentes (isomorfismos, densidades, produtos) e produzir uma prova formal dentro de um assistente de prova (Lean) que não dependa da confiabilidade do solver externo ou da transcrição manual de dados.

Metodologia

Os autores apresentam uma formalização abrangente do método de álgebra de bandeiras de Razborov em Lean 4, estruturada em três camadas distintas e uma investigação metateórica:

1. A Camada de Especificação (Fundamentos Matemáticos)

Esta camada formaliza as definições matemáticas abstratas de álgebras de bandeiras para grafos simples finitos, seguindo de perto a literatura padrão.

• Definições: Define tipos de bandeiras (flags) (classes de isomorfismo de grafos rotulados), bandeiras e a álgebra de bandeiras $A_\sigma$ como um quociente de um espaço vetorial livre por identidades de expansão (derivadas da regra da cadeia).
• Semântica: Define homomorfismos positivos como mapas da álgebra para $\mathbb{R}$ que preservam a estrutura e a não-negatividade. O cone de não-negatividade semântica $C_\sigma$ é definido como o conjunto de elementos não-negativos sob todas essas homomorfismos.
• Semântica Restrita: Ao contrário das apresentações tradicionais que constroem a restrição de grafo proibido $H$ na construção da álgebra, esta formalização constrói a álgebra ambiente de todos os grafos finitos. A condição de ser livre de $H$ é imposta posteriormente via uma "ordem semântica de ensemble". Esta ordem restringe os homomorfismos positivos considerados para aqueles que atribuem densidade zero a grafos que contêm $H$, usando uma medida de extensão aleatória para interpretar desigualdades em bandeiras rotuladas.
• Operador Descendente (Downward Operator): Formaliza o operador que mapeia elementos de álgebra rotulados para não rotulados, provando que ele preserva a não-negatividade semântica (Teorema 2.9).

2. A Camada de Reflexão (Computações Executáveis)

Como a camada de especificação depende de tipos de quociente não computáveis e definições abstratas, uma "camada de reflexão" separada é desenvolvida para realizar os cálculos finitos necessários.

• Representações Concretas: Utiliza estruturas de dados concretas (por exemplo, Sym2Graph com vértices como Fin n e arestas como conjuntos finitos) para representar grafos e bandeiras, permitindo enumeração e igualdade decidível.
• Teoremas de Adequação: O núcleo desta camada consiste em teoremas provando que as computações executáveis (cálculos de densidade, verificações de isomorfismo, fatores de normalização descendente) concordam com as definições abstratas na camada de especificação.
• Metaprogramação: Comandos customizados de elaboração geram bandeiras específicas, tabelas de densidade e tabelas de multiplicação para os tamanhos exigidos por um certificado específico. Estes comandos provam lemas de completude garantindo que todas as classes de isomorfismo relevantes sejam cobertas.

3. O Compilador de Certificado-para-Prova

Este componente automatiza a tradução de certificados de SDP externos em provas de Lean verificadas.

• Entrada: Aceita um certificado JSON do Flagmatic contendo grafos alvo, grafos proibidos, limites propostos, tipos de bandeira e matrizes racionais PSD.
• Processo de Verificação:
  1. Regeneração: Regenera as bandeiras necessárias e as identidades de densidade/multiplicação usando a camada de reflexão, em vez de confiar nos dados do certificado.
  2. Verificação de PSD: Reconstrói as matrizes racionais e verifica sua semidefinitude positiva sobre $\mathbb{Q}$ usando fatorações $LDL^\top$ exatas, evitando aritmética de ponto flutuante.
  3. Montagem Algébrica: Utiliza as identidades verificadas para expandir a identidade algébrica do certificado (decompondo o gap $c \cdot 1 - [F]$ em quadrados descendentes e um resto não-negativo) e verifica a desigualdade final.
• Modelo de Confiança: O script do compilador não é confiável; ele gera uma proposta de prova. O Lean verifica independentemente cada passo, incluindo as fatorações de matriz e a normalização algébrica. O script é apenas confiável para a fidelidade da tradução (mapeamento das bandeiras do certificado para a enumeração do Lean), o que é auditável através da inspeção da declaração do teorema gerado.

4. Meta-Teoria de Semântica Restrita

O artigo investiga a relação entre a "semântica de ensemble" (usada na implementação) e a "semântica de quociente" (onde as restrições são incorporadas).

• Raiz-Plantável (Root-Plantability): Os autores definem um critério chamado "raiz-plantabilidade" para caracterizar quando as duas abordagens semânticas concordam. Eles provam que se uma classe de grafos é "fechada sob blow-up" (por exemplo, grafos livres de $K_r$ para $r \ge 3$), as duas ordens concordam.
• Contraexemplo: Eles fornecem um contraexemplo (grafos livres de $C_4$) onde as ordens diferem, demonstrando que a hereditariedade sozinha é insuficiente para o acordo.

Principais Resultados

Os autores avaliaram o compilador em sete certificados de limite superior distintos, produzindo com sucesso provas verificadas por máquina para:

1. Teorema de Mantel: Provando $\pi(K_2; K_3) = 1/2$.
2. Teorema do Pentágono de Erdős: Provando $\pi(C_5; K_3) = 24/625$. (Nenhuma prova evitando álgebras de bandeiras é conhecida para este resultado).
3. Densidade de $C_4$: Um limite superior para a densidade de $C_4$ em grafos livres de triângulos.
4. Limites de densidade de arestas: Para grafos livres de $K_4$, $K_5$ e $C_5$.

Adicionalmente, a formalização foi usada diretamente (sem o compilador) para:

• Provar os limites inferiores correspondentes ao Teorema de Mantel e ao Teorema do Pentágono de Erdős usando construções explícitas.
• Provar duas desigualdades de Goodman.

Todos os sete certificados foram compilados em arquivos fonte de Lean contendo nenhum sorry ou axioma. Cinco dos sete foram verificados inteiramente por redução de kernel (decide +kernel), enquanto os dois maiores ($K_5$-livre e $C_5$-livre densidade de aresta) exigiram decide nativo devido a limites computacionais, uma limitação que os autores explicitamente reconhecem.

Significância e Alegações

O artigo afirma fornecer a primeira formalização verificada por máquina do método de álgebra de bandeiras para grafos simples finitos, unindo a lacuna entre a busca assistida por computador e a prova rigorosa formal. Sua significância reside em:

• Verificação de Combinatória Complexa: Demonstra que provas de álgebra de bandeiras, que dependem de quantidades massivas de dados finitos exatos e resultados de SDP, podem ser totalmente verificadas em um assistente de prova sem confiar no solver externo ou na transcrição manual.
• Arquitetura Modular: A separação das camadas de especificação (matemática), reflexão (computação) e compilador (automação) oferece um framework reutilizável para formalizar outros problemas extremais.
• Insight Meta-Teórico: A formalização da semântica de ensemble e do critério de raiz-plantabilidade fornece uma compreensão matemática rigorosa das restrições impostas pela implementação, esclarecendo quando a abordagem de "rótulo aleatório" é equivalente à abordagem de "restrição incorporada".
• Novas Provas: Fornece a primeira prova formal do Teorema do Pentágono de Erdős e novas provas formais para as desigualdades de Goodman e limites inferiores para densidades de Turán.

Os autores permanecem modestos sobre as limitações atuais, observando que a abordagem depende de solvers de SDP externos para a descoberta de certificados e que escalar além de cinco vértices enfrenta obstáculos computacionais significativos na verificação checada pelo kernel. Eles veem este trabalho como uma fundação para futuras extensões a hipergrafos, grafos direcionados e a integração da teoria de graphons.