{"id":537862,"date":"2026-04-21T20:00:00","date_gmt":"2026-04-21T23:00:00","guid":{"rendered":"https:\/\/www.portaltela.com\/noticias\/2026\/04\/21\/lean-o-novo-tira-teima-da-matematica\/"},"modified":"2026-04-21T20:00:00","modified_gmt":"2026-04-21T23:00:00","slug":"lean-o-novo-tira-teima-da-matematica","status":"publish","type":"post","link":"https:\/\/www.portaltela.com\/noticias\/ciencia\/2026\/04\/21\/lean-o-novo-tira-teima-da-matematica\/","title":{"rendered":"Lean, o novo tira-teima da matem\u00e1tica"},"content":{"rendered":"<p>Lean, novo tira-teima da matem\u00e1tica<\/p>\n<p>Um novo recurso interativo aproxima matem\u00e1ticos e m\u00e1quinas na verifica\u00e7\u00e3o de teoremas. Criada por brasileiro, a ferramenta facilita a colabora\u00e7\u00e3o entre humano e software para validar provas.<\/p>\n<p>A iniciativa tem como foco a redu\u00e7\u00e3o de lacunas causadas pela complexidade de demonstra\u00e7\u00f5es cada vez maiores. Ela utiliza uma biblioteca de teoremas j\u00e1 verificados para apoiar novas provas.<\/p>\n<p>O sistema Lean funciona como uma linguagem de programa\u00e7\u00e3o e verificador de teoremas desenvolvido na Microsoft Research. O pesquisador formula o teorema e envia comandos simples para que o software confirme cada etapa.<\/p>\n<p>Ao longo do processo, o Lean identifica suposi\u00e7\u00f5es, sinaliza lacunas l\u00f3gicas e, ao fim, declara a veracidade da prova. A abordagem evita refazer os passos a cada passo, conectando-os a fundamentos j\u00e1 validados.<\/p>\n<p>A biblioteca MathlLib agrega centenas de milhares de teoremas, contidos em mais de 2 milh\u00f5es de linhas de c\u00f3digo Lean. Essas formaliza\u00e7\u00f5es ajudam a justificar proposi\u00e7\u00f5es novas com maior confiabilidade.<\/p>\n<p>Especialistas veem grande potencial no uso dessa metodologia. Entre eles, Terence Tao, ganhador da medalha Fields, que j\u00e1 desenvolveu uma ferramenta pr\u00f3pria para apoiar sua pesquisa.<\/p>\n<p>No come\u00e7o de 2024, Tao e Alex Kontorovich lan\u00e7aram o desafio de transcrever para Lean o Teorema dos N\u00fameros Primos. Em janeiro de 2025, a Math, Inc. afirmou ter vencido parcialmente esse desafio com aux\u00edlio de intelig\u00eancia artificial.<\/p>\n","protected":false},"excerpt":{"rendered":"<ul>\n<li>Lean \u00e9 uma linguagem de programa\u00e7\u00e3o e verificador de teoremas, criado na Microsoft Research em 2013, com colabora\u00e7\u00e3o direta entre matem\u00e1tico e m\u00e1quina.<\/li>\n<li>O formalismo permite decompor provas em passos simples, at\u00e9 confirmar a veracidade do teorema de forma autom\u00e1tica.<\/li>\n<li>A MathLlib (biblioteca de Lean) j\u00e1 re\u00fane centenas de milhares de teoremas, em mais de 2 milh\u00f5es de linhas de c\u00f3digo.<\/li>\n<li>O brasileiro Leonardo de Moura foi um dos criadores e destaque, defendendo o uso colaborativo entre humano e m\u00e1quina.<\/li>\n<li>Em janeiro de 2024, Terence Tao e Alex Kontorovich desafiaram transcrever para Lean o Teorema dos N\u00fameros Primos; no m\u00eas passado, a empresa Math, Inc. afirmou ter vencido esse desafio com aux\u00edlio de intelig\u00eancia artificial.<\/li>\n<\/ul>\n","protected":false},"author":15,"featured_media":537871,"comment_status":"closed","ping_status":"closed","sticky":false,"template":"","format":"standard","meta":{"summary":"Lean permite colabora\u00e7\u00e3o entre matem\u00e1tico e m\u00e1quina na verifica\u00e7\u00e3o de teoremas, com a biblioteca MathlLib j\u00e1 contendo centenas de milhares de teoremas em mais de 2 milh\u00f5es de linhas","footnotes":""},"categories":[296,1],"tags":[169,85,105,98,189,99],"class_list":["post-537862","post","type-post","status-publish","format-standard","has-post-thumbnail","hentry","category-ciencia","category-noticias","tag-cientistas","tag-inovacao","tag-inteligencia-artificial","tag-pesquisa","tag-tecnologia","tag-universidades"],"_links":{"self":[{"href":"https:\/\/www.portaltela.com\/api\/wp\/v2\/posts\/537862","targetHints":{"allow":["GET"]}}],"collection":[{"href":"https:\/\/www.portaltela.com\/api\/wp\/v2\/posts"}],"about":[{"href":"https:\/\/www.portaltela.com\/api\/wp\/v2\/types\/post"}],"author":[{"embeddable":true,"href":"https:\/\/www.portaltela.com\/api\/wp\/v2\/users\/15"}],"replies":[{"embeddable":true,"href":"https:\/\/www.portaltela.com\/api\/wp\/v2\/comments?post=537862"}],"version-history":[{"count":0,"href":"https:\/\/www.portaltela.com\/api\/wp\/v2\/posts\/537862\/revisions"}],"wp:featuredmedia":[{"embeddable":true,"href":"https:\/\/www.portaltela.com\/api\/wp\/v2\/media\/537871"}],"wp:attachment":[{"href":"https:\/\/www.portaltela.com\/api\/wp\/v2\/media?parent=537862"}],"wp:term":[{"taxonomy":"category","embeddable":true,"href":"https:\/\/www.portaltela.com\/api\/wp\/v2\/categories?post=537862"},{"taxonomy":"post_tag","embeddable":true,"href":"https:\/\/www.portaltela.com\/api\/wp\/v2\/tags?post=537862"}],"curies":[{"name":"wp","href":"https:\/\/api.w.org\/{rel}","templated":true}]}}