Por que não usar apenas Lean?

• A história da formalização da matemática não começou com Lean, e diferentes linhagens de sistemas já vinham acumulando técnicas centrais e resultados importantes há quase 60 anos
• Ferramentas como AUTOMATH de 1968, a família LCF, HOL, Rocq, ACL2 e Mizar produziram formalizações amplas, da análise real ao teorema dos números primos, ao teorema das quatro cores e à conjectura de Kepler
• Lean construiu rapidamente definições da matemática moderna com base em uma grande biblioteca e em 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, além de manter a tradição LCF de estruturar a verificação de provas pela barreira de abstração do kernel, mesmo sem proof objects
• Com a ascensão da IA para organizar provas estruturadas e até traduzir entre sistemas diferentes, a pressão para tratar uma única ferramenta como padrão absoluto pode diminuir ainda mais no futuro

---

Sistemas iniciais e outras linhagens

• AUTOMATH

  • AUTOMATH já incluía em 1968 a maior parte dos elementos necessários para a formalização da matemática
  • Em 1977, Jutting formalizou em AUTOMATH o Foundations of Analysis de Landau e foi da lógica pura até a construção dos números complexos
  • Ele usou classes de equivalência e o conjunto dos racionais, e também provou formalmente a completude de Dedekind da reta real
  • Esse feito não voltou a aparecer por 20 anos, e só em meados dos anos 1990 a formalização dos reais reapareceu em HOL Light, de John Harrison, e em 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, considera-se que ele era melhor que Rocq ao lidar com classes de equivalência e, ao contrário do inferno dos setoids enfrentado por usuários de Rocq, Jutting realizou a formalização com classes de equivalência de forma serena

• Boyer e Moore

  • A computational logic da linhagem de Robert Boyer e J Moore surgiu visando 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 assistente de provas se difundiu amplamente
• Vários grupos, em Cambridge, INRIA, Cornell e outros lugares, criaram ferramentas iniciais como HOL, Coq (hoje Rocq) e Nuprl usando ML
• O grupo HOL focava em verificação de hardware, mas a verificação de hardware de ponto flutuante passou a exigir análise real
• John Harrison provou em sistemas da família HOL resultados matemáticos robustos como o teorema dos números primos, via a fórmula integral de Cauchy
• Sob o objetivo de verificar o máximo possível dos 100 theorems, HOL Light frequentemente ficou entre os primeiros colocados
• Até 2014, sistemas dessa linhagem haviam formalizado vários teoremas avançados
  • o teorema das quatro cores
  • o odd order theorem
  • a consistência relativa do axioma da escolha
  • o segundo teorema da incompletude de Gödel
  • a conjectura de Kepler de Tom Hales
• Em geral, esses teoremas tinham provas longas e complexas, e os trabalhos de formalização eram de grande escala, desempenhando um papel crucial na redução de dúvidas remanescentes sobre os teoremas

A ascensão da comunidade Lean

• Matemáticos entendiam que os resultados anteriores de formalização não alcançavam construções sofisticadas da matemática moderna dominante como Grothendieck schemes ou perfectoid spaces
• Tom Hales escolheu então a direção de acumular essas definições em biblioteca, focando mais na acumulação de definições do que em provas, e escolheu Lean
• 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, o que acelerou sua difusão depois
• Como ponto importante de virada da comunidade Lean, aponta-se o afastamento da antiga obsessão com prova construtiva que dominou Rocq por muito tempo
• O intuicionismo surgiu após o paradoxo de Russell e também tinha implicações específicas para o conceito de números reais
• A teoria dos tipos de Martin-Löf é claramente um formalismo intuicionista, mas o texto diz que Rocq não pode ser visto de forma tão simples
• Ainda assim, em artigos ligados a Rocq, a prova construtiva aparecia repetidamente até em contextos onde era irrelevante ou sem sentido, e considera-se que essa tendência atrapalhou a aplicação de Rocq à matemática e cedeu espaço a Lean

propositions as types e a diferença do LCF

• Propositions as types é a dualidade que conecta os símbolos lógicos ∀, ∃, →, ∧, ∨ aos construtores de tipo Π, Σ, →, ×, +
• Essa estrutura é bela e teoricamente produtiva, mas não é o único caminho
• Se um proof assistant for definido apenas como software que verifica provas segundo o princípio de propositions as types, boa parte da pesquisa dos últimos 50 anos fica fora da definição
• Nesse caso, restariam apenas Rocq, Lean e Agda
• Até o próprio AUTOMATH não é um caso de propositions as types; embora tenha elementos parecidos com Π e →, sua lógica é configurada como axiomas, como em livros comuns 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), o que exige proof irrelevance
• Também se afirma explicitamente que a percepção de que a abordagem LCF é igual a propositions as types não corresponde aos fatos
  • 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 elimina objetos de prova gigantes; eles continuam existindo no sistema real
• A descoberta central de Robin Milner foi que, em LCF, o próprio objeto de prova não é necessário
• Colocando o kernel de prova dentro de um tipo de dado abstrato de ML e usando regras de inferência como construtores, é possível verificar provas dinamicamente
• Graças à barreira de abstração de ML, considera-se que trapacear é impossível
• Na era do RAMmageddon, parece especialmente irracional que termos gigantes ocupem dezenas de MB sem sequer indicar algo
• O texto também critica o fato de haver pesquisas dedicadas a tornar mais elegantes esses termos desnecessários

Motivos para escolher Isabelle

• Se seus colegas usam Lean, se a especialização da equipe está em Lean e se as bibliotecas de pré-requisitos de que você precisa estão em Lean, então é natural usar Lean
• Ainda assim, se houver liberdade de escolha, há motivos claros para considerar Isabelle

• Automação

  • Sua vantagem seria a automação mais poderosa, e avalia-se que, mesmo comparado aos “hammers” do dia a dia, nada rivaliza com o sledgehammer
  • Observa-se também que a parte de álgebra computacional deveria ser tratada separadamente

• Legibilidade

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

• Evitar tipos dependentes

  • Por não ter tipos dependentes, evita níveis de universo e várias esquisitices que confundem iniciantes
  • O texto afirma que até em mathlib do Lean e em SSReflect e Mathematical Components do Rocq o uso de tipos dependentes não é recomendado
  • A principal dificuldade dos tipos dependentes é que, se implementados corretamente, a própria checagem de tipos se torna indecidível
  • Isso ocorre porque a decisão de igualdade é indecidível, e diz-se que esse ponto foi inicialmente aceito como natural
  • Por volta de 1990, o consenso mudou para tornar a checagem de tipos decidível, reduzindo a igualdade a 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 checagem de igualdade definicional ainda tem alto custo computacional

Matemática moderna possível mesmo sem tipos dependentes

• O texto afirma que, em 2017, via com muito mais cautela até onde Isabelle conseguiria ir em matemática
• Na época, era fácil parecer que tipos dependentes eram indispensáveis para temas como os seguintes
  • extensões de corpos
  • números p-ádicos
  • Grothendieck schemes
• Mas muito foi aprendido com a pesquisa relacionada ao Alexandria, e a conclusão é que o essencial é não empurrar tudo para dentro dos tipos

Direção futura e IA

• Lean acertou muita coisa e, com suporte até para blocos de prova aninhados, pode se tornar uma linguagem de prova suficientemente legível em potencial
• Agora a comunidade Lean precisa usar esses recursos na prática, e o texto diz que usuários de Isabelle já fazem isso em grande medida
• Mais importante do que objetos de prova verificáveis por computador é a transparência do texto da prova que pessoas realmente conseguem ler
• 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 detalhes em excesso
• Assim, fica mais fácil entender o fluxo do argumento e reduzi-lo a uma forma mais simples
• Recentemente também apareceu pesquisa em que modelos de linguagem chamam diretamente o sledgehammer
• A IA também poderá traduzir facilmente provas estruturadas e legíveis de um proof assistant para outro
• Se isso acontecer, a própria pressão sobre qual sistema escolher diminuirá

Complemento sobre a ausência de Mizar

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

[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