Por que não usar simplesmente Lean?

• A história da formalização matemática não começou com Lean; por quase 60 anos, vários sistemas de diferentes linhagens já vinham acumulando técnicas centrais e resultados importantes
• Ferramentas como AUTOMATH de 1968, a família LCF, HOL, Rocq, ACL2 e Mizar realizaram formalizações amplas, da análise real ao teorema dos números primos, o teorema das quatro cores e a conjectura de Kepler
• Lean construiu rapidamente definições da matemática moderna com base em uma grande biblioteca e uma comunidade ativa, mas propositions as types e tipos dependentes não são o único caminho para proof assistants
• Isabelle destaca automação forte, alta legibilidade e a evasão de tipos dependentes como vantagens, mantendo a tradição LCF de construir verificação de provas com a barreira de abstração do kernel, mesmo sem proof objects
• Com a ascensão da IA organizando provas estruturadas e até traduzindo-as entre sistemas, a pressão para ver uma única ferramenta como padrão absoluto pode diminuir ainda mais no futuro

---

Sistemas iniciais e outras linhagens

• AUTOMATH

  • AUTOMATH já continha em 1968 a maior parte dos elementos necessários para a formalização matemática
  • Em 1977, Jutting formalizou com AUTOMATH o Foundations of Analysis de Landau, partindo da lógica pura e chegando até a construção dos números complexos
  • Usou classes de equivalência e o conjunto dos números racionais, e também provou formalmente a completude de Dedekind da reta real
  • Esse feito não voltou a aparecer por 20 anos; só em meados dos anos 1990 a formalização dos reais foi retomada no HOL Light de John Harrison e no Isabelle/HOL de Jacques Fleuriot
  • A notação era muito incômoda e não havia automação alguma, então as provas eram longas e difíceis de ler
  • Ainda assim, o autor considera que ele lidava melhor com classes de equivalência do que Rocq; ao contrário do inferno dos setoids enfrentado por usuários de Rocq, Jutting realizou a formalização de classes de equivalência com serenidade

• Boyer e Moore

  • A linhagem de lógica computacional de Robert Boyer, J Moore surgiu mirando verificação de código, não matemática
  • Essa direção apareceu pela primeira vez no artigo de 1973 Proving theorems about LISP functions
  • Havia limitações claras para matemática geral, mas ela também foi usada para formalizar resultados profundos como o teorema da incompletude de Gödel, a reciprocidade quadrática e o teorema de Banach–Tarski
  • Sua linhagem atual, ACL2, é aplicada principalmente à verificação de hardware

O fluxo após LCF

• Edinburgh LCF era focado em teoria de linguagens de programação, mas a ideia de usar uma linguagem funcional como metalinguagem de um proof assistant se difundiu amplamente
• Grupos em Cambridge, INRIA, Cornell e outros lugares usaram ML para criar ferramentas como HOL inicial, Coq (hoje Rocq) e Nuprl
• O grupo HOL concentrou-se em verificação de hardware, mas a verificação de hardware de ponto flutuante acabou exigindo análise real
• John Harrison provou na linhagem HOL resultados matemáticos substanciais como o teorema dos números primos, via fórmula integral de Cauchy
• Sob a meta de verificar o máximo possível dos 100 teoremas, HOL Light frequentemente apareceu entre os líderes
• Até 2014, os sistemas dessa linhagem haviam formalizado vários teoremas avançados
  • Teorema das quatro cores
  • odd order theorem
  • Consistência relativa do axioma da escolha
  • Segundo teorema da incompletude de Gödel
  • Conjectura de Kepler de Tom Hales
• Essas demonstrações em geral eram longas e complexas, e os trabalhos de formalização também foram de escala muito grande, tendo papel crucial em reduzir dúvidas remanescentes sobre os teoremas

A ascensão da comunidade Lean

• Matemáticos consideravam que as conquistas anteriores de formalização não alcançavam construções sofisticadas da matemática moderna dominante como Grothendieck schemes e perfectoid spaces
• Tom Hales escolheu seguir o caminho de acumular essas definições em bibliotecas e optou por Lean, com foco na acumulação de definições mais do que nas provas
• Ele apresentou essa direção no programa Big Proof, onde ideias semelhantes também foram discutidas
• Kevin Buzzard ouviu isso e decidiu experimentar Lean no ensino, acelerando depois a disseminação
• Um ponto de inflexão importante para a comunidade Lean foi, segundo o texto, afastar-se da obsessão com provas construtivas que dominou Rocq por muito tempo
• O intuicionismo surgiu após o paradoxo de Russell e teve implicações específicas também para o conceito de número real
• A teoria dos tipos de Martin-Löf é claramente um formalismo intuicionista, mas o texto observa que Rocq não pode ser visto de forma tão simples
• Ainda assim, artigos ligados a Rocq repetiam provas construtivas até em contextos onde eram irrelevantes ou sem sentido; o autor avalia que essa tendência travou a aplicação de Rocq à matemática e abriu espaço para Lean

propositions as types e a diferença da LCF

• Propositions as types é a dualidade que liga os símbolos lógicos ∀, ∃, →, ∧, ∨ aos construtores de tipos Π, Σ, →, ×, +
• Esse arcabouço é belo e teoricamente produtivo, mas não é o único caminho
• Se um proof assistant for definido apenas como software que verifica provas pelo princípio de propositions as types, a maior parte da pesquisa do último meio século fica excluída da definição
• Nesse caso, só restariam Rocq, Lean e Agda
• Até o próprio AUTOMATH não é um caso de propositions as types; embora tenha elementos parecidos com Π e →, ele estabelece a lógica como axiomas, como em um manual comum de lógica
• De Bruijn já via há 50 anos a necessidade de separar tipos e proposições
• Um exemplo típico é a divisão, que deveria receber três argumentos, e o valor de (x/y) dependeria de uma prova de (y \ne 0), tornando necessária a proof irrelevance
• O texto também afirma categoricamente que a ideia de que a abordagem LCF é igual a propositions as types está errada
  • Texto sobre LCF
• Rocq e Lean têm o sort de proposições Prop, no qual todos os objetos de prova da mesma proposição são avaliados como o mesmo valor, fornecendo proof irrelevance
• Isso não faz com que proof objects gigantes desapareçam; eles continuam existindo nos sistemas reais
• A descoberta central de Robin Milner foi que em LCF os próprios proof objects não são necessários
• Colocando o kernel de provas dentro de um tipo de dado abstrato de ML e tratando as regras de inferência como construtores, é possível verificar provas dinamicamente
• Graças à barreira de abstração do ML, não haveria como trapacear
• Na era do RAMmageddon, parece especialmente irracional que termos gigantescos ocupem dezenas de MB mesmo sem apontar para nada
• O texto também critica o fato de haver pesquisa dedicada a tornar esses termos desnecessários apenas mais elegantes

Motivos para escolher Isabelle

• Se seus colegas usam Lean, se a especialidade da equipe está em Lean e se a biblioteca de pré-requisitos de que você precisa também está em Lean, é natural usar Lean
• Mas, se for possível escolher livremente, há razões claras para considerar Isabelle

• Automação

  • O texto aponta a automação mais poderosa como vantagem e avalia que, mesmo comparado aos “hammers” cotidianos, nada se equipara ao sledgehammer
  • Ele acrescenta que a área de álgebra computacional também mereceria discussão separada

• Legibilidade

  • Isabelle é colocado como a melhor opção em legibilidade, com base em exemplos relacionados ao Isar

• Evasão de tipos dependentes

  • Por não ter tipos dependentes, evita universe levels e várias peculiaridades que confundem iniciantes
  • O texto afirma que o uso de tipos dependentes também não é recomendado no mathlib do Lean nem em SSReflect e Mathematical Components do Rocq
  • A dificuldade central dos tipos dependentes é que, se forem implementados corretamente, a própria checagem de tipos se torna indecidível
  • Isso ocorre porque a decisão de igualdade é indecidível, e no início isso era tratado como algo natural
  • Por volta de 1990, formou-se um consenso em direção a tornar a checagem de tipos decidível rebaixando a igualdade para definitional/intensional equality
  • Como resultado, (T(N+1)) e (T(1+N)) passam a ser tipos diferentes
  • Essa limitação afeta provas reais, e a própria verificação de definitional equality ainda traz alto custo computacional

Matemática moderna possível mesmo sem tipos dependentes

• O texto diz que, em 2017, era muito mais cauteloso sobre até onde Isabelle conseguiria ir em matemática
• Na época, parecia fácil supor que temas como os seguintes exigiriam necessariamente tipos dependentes
  • Extensões de corpos
  • Números p-ádicos
  • Grothendieck schemes
• Porém, os estudos ligados ao projeto Alexandria ensinaram muito, e a conclusão central foi não empurrar tudo para dentro dos tipos

Direções futuras e IA

• Lean acertou muita coisa e, com suporte até a blocos de prova aninhados, tem potencial para se tornar uma linguagem de provas suficientemente legível
• Agora a comunidade Lean precisa realmente usar esses recursos, enquanto os usuários de Isabelle, segundo o texto, em geral já fazem isso
• A transparência do texto da prova que pessoas de fato conseguem ler é mais importante do que proof objects verificáveis por computador
• A ascensão da IA torna essa diferença ainda mais nítida
• Provas geradas por IA costumam ser bagunçadas, mas são fáceis de organizar com sledgehammer, e, se a estrutura estiver bem montada, continuam legíveis mesmo com excesso de detalhes
• Isso facilita acompanhar o fluxo do argumento e reduzi-lo depois a uma forma mais simples
• Recentemente também apareceu pesquisa em que modelos de linguagem chamam diretamente o sledgehammer
• A IA também pode facilmente traduzir provas estruturadas e legíveis de um proof assistant para outro
• Se isso acontecer, a própria pressão de escolher um sistema específico diminui

Correção da omissão de Mizar

• A história da formalização matemática não fica completa sem Mizar e sua vasta biblioteca matemática
• A linguagem Isar do Isabelle também recebeu forte influência de Mizar
• O texto corrige separadamente a omissão de Mizar e diz que o próximo artigo tratará de Mizar

[GN⁺]

Comentários do Hacker News

• Como a maioria dos leitores do HN está mais para programadores do que para matemáticos, parece mais prático olhar para Lean pela perspectiva da programação do que pela de provas matemáticas
  Um livro bem bom para abordar Lean pela ótica de programação funcional é https://leanprover.github.io/functional_programming_in_lean/
  Eu também estou aprendendo Lean, então talvez tenha um pouco de visão cor-de-rosa de iniciante, mas meu objetivo é ir na direção de escrever e provar código de programador comum, como algoritmos reais de compressão/descompressão, como no exemplo recente do lean-zip
  https://github.com/kiranandcode/lean-zip/blob/master/Zip/Nat...

  • Lendo esse livro, cheguei a brincar de implementar um simplificador básico de álgebra computacional em Lean
    https://github.com/dharmatech/symbolism.lean
    É um port de código em C#, e a expressividade de Lean é impressionantemente grande
  • Para esse tipo de uso, imagino que Dafny também seja uma opção parecida
    Vi algum burburinho sobre isso um tempo atrás, mas não tenho acompanhado a área de perto recentemente
  • Lembro de um caso nos anos 1990 em que experimentaram provas de correção de software, e pelo que me lembro o comentário final da prova tinha mais erros do que o software em si
    E ainda vejo mais dois obstáculos. Primeiro, já é difícil saber o que o software deve fazer, e o que o usuário quer nem sempre é a mesma coisa que aquilo pelo qual o cliente paga
    Segundo, a qualidade do trabalho de muitos desenvolvedores é tão baixa que é difícil esperar que lidem melhor com uma linguagem da verdade do que com uma linguagem como Java
    Mas o segundo ponto talvez desapareça com a substituição por sistemas de IA que prestem a atenção necessária, e aí o cenário pode mudar
  • Fico pensando em como fica a programação não funcional
    Também acho que programação funcional já é, para a maioria dos programadores, tão pouco relevante quanto a matemática que eles já deixaram de lado

• O autor parece ter entendido Lean bastante mal, o que surpreende ainda mais porque ele parece alguém que conhece bem essa área
  Ele parece achar que Lean preserva os objetos de prova como estão e, no fim, verifica um único objeto de prova gigantesco com todas as definições expandidas, mas isso está longe da realidade
  Lean implementa praticamente a mesma otimização que o autor elogia como vantagem do LCF. Numa analogia, é como ir apagando o quadro-negro à medida que a prova avança
  No Lean4, se você escreve com theorem em vez de def, esse objeto de prova deixa de ser usado, e isso não é uma simples otimização, mas uma propriedade central da linguagem. theorem é opaque
  Mesmo que o termo da prova permaneça, isso serve apenas para que o usuário possa vê-lo no modo interativo, e o kernel nem sequer pode se importar com qual era esse objeto de prova

  • Isso parece mais uma diferença conceitual do que de implementação
    Em LCF, prova e termo são coisas diferentes, e na minha opinião originalmente deveria ser assim. Essa confusão ao estilo Curry-Howard é desnecessária, mas muita gente acha que esse é o único jeito de fazer matemática no computador
    Se quiser, você também pode armazenar e usar provas em LCF, e em Lean também pode eliminá-las por otimização se quiser
  • Em teoria de tipos dependentes, o objeto de prova é simplesmente o próprio termo que preenche um tipo; sendo assim, fico curioso se isso significa que a implementação de Lean consegue construir provas sem criar esse tipo de termo
  • Parece correto
    A abordagem de tipo abstrato talvez economize um pouco de memória, mas isso seria só uma diferença de fator constante, não uma melhora assintótica
    Reclamações de que Lean desperdiça dezenas de MB talvez fossem importantes nos anos 1980–90, mas hoje isso talvez já não seja uma vantagem tão decisiva

• Ouço muito que Lean é bom para programação funcional, mas vindo de Agda ele parece um downgrade meio grosseiro
  Também dizem que as tactics são boas, mas na minha experiência as tactics do Coq eram mais poderosas e mais fáceis de usar
  Pode ser tudo viés de primeira impressão, mas até agora parece que a força de Lean não vem de fazer uma coisa melhor do que todos, e sim de ser razoavelmente bom no geral e ter uma comunidade grande
  Entendo por que isso é atraente, mas também dá uma sensação de que um pouco da beleza e da força se perderam nesse processo

  • No fim, isso também é uma questão de efeito de rede
    Só que esse tipo de efeito parece permanente quando está acontecendo, mas na prática não dura tanto quanto se imagina. Se fosse só isso que importasse, Perl ainda seria um gigante hoje
    No caso de Lean, pesa muito o fato de ele ter conseguido antes uma biblioteca grande. É parecido com o papel que o CPAN teve para Perl
    Mas, olhando para leis de escala, o valor de uma biblioteca grande para a maioria dos usuários provavelmente cresce algo mais próximo do logaritmo do tamanho
    https://pdodds.w3.uvm.edu/teaching/courses/2009-08UVM-300/do...
    No começo essa diferença parece impossível de superar, mas em algum ponto não é mais necessário alcançar o mesmo tamanho, porque usabilidade passa a importar mais
    Além disso, portar bibliotecas matemáticas é justamente um tipo de tarefa que combina bem com LLMs. A fonte já foi verificada, o destino também pode ser verificado, e o caminho de raciocínio em geral também pode ser transportado
    Dito de outro modo, os LLMs também reduzem mais do que se esperava a barreira de trabalhar em plataformas menores. Se eu consigo portar a biblioteca deles para a minha plataforma, talvez eu também consiga portar minhas provas para lá
  • Na verdade isso me parece mais um sinal de que a comunidade finalmente amadureceu e começou a fazer trabalho de verdade
    A questão não é ter a ferramenta perfeita, e sim conseguir fazer o trabalho com uma ferramenta boa o bastante
  • Agda é melhor como verificador de provas, mas eu não o vejo como uma opção prática para construir software
    Lean parece ter espaço para crescer como linguagem funcional voltada a desenvolvimento de software, a ponto de talvez se tornar um verdadeiro sucessor de Haskell
  • Usei um pouco Agda e mais Lean, e para escrever programas funcionais gerais, não provas matemáticas, Lean foi muito mais fácil
    Acho que a diferença veio principalmente do suporte de ferramentas. A documentação do Agda é fraca, instalar e fazer o sistema funcionar é incômodo, e ele praticamente exige que você use Emacs
    Já Lean tem até documentação própria ensinando a escrever um utilitário cat, e no geral entrega uma experiência de tooling bem mais moderna
  • Fico curioso sobre o que exatamente há de tão bom na programação funcional em Agda
    Normalmente ouço elogios mais pelo lado de dependent pattern matching, e nisso sinto que Lean é bem fraco
    Ainda assim, se você sente que Agda também é mais amigável para FP em geral, queria entender em que aspectos

• Isabelle/HOL até tem uma linguagem razoável, mas o tooling tem falhas profundas que vão além da abordagem centrada em desktop
  A linguagem não é tão diferente de Lean nem necessariamente melhor, e concordo com algumas críticas a tipos dependentes
  No fim, as duas linguagens fizeram trade-offs diferentes, e essas escolhas parecem tê-las tornado ferramentas bem eficientes em seus respectivos espaços. O domínio de provas é amplo, então cada paradigma tem forças e fraquezas diferentes, e Lean apenas se especializou em outra parte dele
  Sledgehammer é bom, mas parece só questão de tempo até Lean ter algo parecido
  Na fase de exploração isso pode ser útil, mas consome muitos recursos e, embora encurte a prova, em código publicado eu prefiro ver todos os passos da prova explicitamente em vez de um by sledgehammer meio mágico
  Por outro lado, desenvolver o próprio Isabelle é muito mais doloroso do que desenvolver Lean, especialmente no processo de comunicação com os desenvolvedores
  A atitude em listas de e-mail de que não existem bugs, só comportamentos inesperados pareceu infantil e antiprofissional
  E zombar do uso de RAM de sistemas parecidos com Lean também soa meio ridículo quando se olha para a própria fome de memória do Isabelle

  • O problema aqui é que transformar certificados UNSAT em uma forma que possa ser verificada rapidamente não é nada trivial
    Na prática isso tem dificuldade parecida com a de usar provas formais em si
  • Da última vez que vi, lembro que Isabelle/HOL usava um modo customizado de Emacs como interface
    Posso estar confundindo com outro HOL
  • Não sei exatamente o que é Sledgehammer, mas pela descrição parece quase a mesma coisa que a grind do Mathlib
    https://leanprover-community.github.io/mathlib4_docs/Init/Gr...

• O ponto interessante em Lean é que Lean é a linguagem, mas o que as pessoas realmente discutem na maior parte do tempo é a biblioteca Mathlib
  Os criadores do Mathlib parecem bastante pragmáticos, então eles colocam lógica clássica dentro dos tipos de Lean e usam lógica intuicionista só em parte

  • O exemplo usado para explicar o terceiro excluído estava errado
    “Algo não pode ser ao mesmo tempo verdadeiro e falso” não é terceiro excluído, mas sim a lei da não contradição
    Terceiro excluído quer dizer que p é verdadeiro ou not p é verdadeiro
    https://en.wikipedia.org/wiki/Law_of_noncontradiction
  • O pessoal de ciência da computação agora está montando sua própria CSLib
    https://www.cslib.io https://www.github.com/leanprover/cslib
    O sentido da lógica intuicionista é, essencialmente, transformar argumentação matemática em construções computáveis, então é interessante ver como vão lidar com isso
    Na verdade, no momento em que você escreve algoritmos em Lean, já entrou de alguma forma em restrições construtivas, e talvez esse nível de lógica já seja suficiente para esse objetivo
  • Lembrei da piada sobre as 5 fases de aceitar a matemática construtiva
    negação, raiva, barganha, depressão, aceitação
    Também vale ver a palestra e o texto relacionados de Andrej Bauer
    https://www.youtube.com/watch?v=21qPOReu4FI
    http://dx.doi.org/10.1090/bull/1556
  • Aqui o correto não seria intuitive logic, mas intuitionistic logic
  • Mesmo com tantas restrições e bloqueios, fico curioso sobre quando e por que alguém passa a preferir lógica intuicionista

• Acho que precisamos de mais textos assim
  Mesmo contra esse pensamento de grupo em que todos empurram é só usar X como se fosse óbvio, sempre existem ao menos razões convincentes para considerar alternativas
  Mesmo que no fim você descarte as alternativas e escolha o mainstream, é melhor fazer isso conhecendo o terreno

  • Não concordo totalmente
    Já criamos frameworks e alternativas demais, e provavelmente muito disso acontece porque é divertido
    Em vez de melhorar as ferramentas existentes ou simplesmente avançar com trabalho real, muita gente vai ampliando sem parar a quantidade de linguagens, bibliotecas e ferramentas de build
    Acho que seria melhor se tivéssemos só metade das linguagens, bibliotecas e ferramentas de build que temos hoje
  • No fim depende do contexto
    Quanto mais você se afasta do mainstream, menos documentação há, mais bugs aparecem em cantos menos explorados e menos gente existe para ajudar
    Quando você já acumulou mais de vinte opções, em média faz sentido escolher a opção padrão e seguir em frente. Atenção é um recurso finito; se você for escrever um relatório de investigação para cada dependência, não sobra foco para resolver o problema principal
    Há duas exceções: quando a ferramenta padrão realmente não serve para o meu caso de uso, ou quando a própria ferramenta padrão se sobrepõe fortemente ao problema central que estou tentando resolver

• Esse tipo de discussão me lembra textos que apontam as limitações do Python em computação científica
  Quando uma comunidade em torno de uma ferramenta razoavelmente boa passa da massa crítica, isso acaba superando a maioria dos outros fatores
  O impulso cresce, tutoriais, textos explicativos e documentação melhor vão se acumulando, e ela basicamente atinge velocidade de escape
  Lean parece estar exatamente nessa posição agora, com até um apoiador fortíssimo como Terrance Tao
  Por isso, dizer que “a linguagem X é melhor” não é totalmente errado, mas pode facilmente perder a pergunta realmente importante
  O ponto central é se ela é de fato melhor do que a ferramenta que todo mundo conhece, consegue usar imediatamente e na qual mais tempo está sendo investido para melhoria
  No fim, parece um caso de worse is better, ou de que ser bom e popular já basta

  • Acho um bom ponto que os LLMs podem tornar bastante eficaz a tradução entre sistemas formais diferentes
    Especialmente porque, nessa área, o resultado da tradução pode em boa parte ser validado automaticamente, então a escolha em si talvez não seja tão problemática
  • Mas, na era da IA, a importância de massa crítica é muito menor
    A IA consegue escrever código mesmo sem uma biblioteca comunitária gigantesca, e lê diretamente documentação e especificações sem precisar que existam um milhão de tutoriais na internet
    Também não há necessidade de evitar linguagens sem mercado de trabalho. A IA não está construindo carreira; ela só precisa fazer a tarefa do momento
    Então linguagens pequenas e DSLs que antes não teriam chance passam a ter mais espaço para adoção
    Acho que a velha monocultura de linguagens da programação pode acabar por causa da IA

• Dizer que “quase tudo o que hoje foi formalizado em qualquer sistema também poderia ter sido formalizado em AUTOMATH” é como dizer que tudo o que hoje se programa em linguagens modernas também poderia ter sido feito em assembly há 50 anos
  Tecnicamente é verdade, mas economicamente é uma realidade completamente diferente

  • Linguagens assembly em geral são Turing-completas, mas não sei bem qual seria a comparação exata correspondente no lado dos motores de prova

• Uns 15 anos atrás, tentei mexer em Coq/Rocq e algumas outras ferramentas, mas tive enorme dificuldade de entender o software em si, mais até do que os conceitos
  O estranho em assistentes de prova/teoremas interativos é que, por causa do caráter interactive, eles acabam sendo uma combinação de linguagem e IDE, e de fato os dois ficam fortemente acoplados
  Então é difícil falar só da linguagem isoladamente; também é preciso considerar em que ambiente ela é usada
  Eu também não sou um fã fanático do VS Code, mas é inegável que uma IDE extensível usada por tanta gente, lapidada com tanto investimento, está muito à frente dos ambientes das alternativas
  Caminhos de entrada excelentes como o Natural Numbers Game parecem possíveis justamente por causa da hackeabilidade e do ecossistema do VS Code
  Ainda assim, algo que me preocupa ao aprender Lean é que a extensibilidade sintática é uma faca de dois gumes
  Depois que você aprende a linguagem, quer conseguir ler código escrito nela; mas se cada projeto começa a criar um monte de DSLs próprias, isso pode sair do controle
  No fim, isso depende de quanta moderação a comunidade e o ecossistema vão ter, então observo isso com um misto de esperança e preocupação

• Lean não é o assistente de provas mais amado pelos matemáticos, nem a ferramenta mais adequada para verificação formal de software
  Mas ele dá conta mais ou menos dos dois e, em troca, capturou o momentum que é mais difícil de obter
  Além disso, na era da IA, a quantidade de código público escrito por humanos afeta diretamente o quão bem agentes conseguem produzir código novo, o que fortalece ainda mais esse momentum