Prova de computador 'explode' equações de fluidos centenárias PlatoBlockchain Data Intelligence. Pesquisa vertical. Ai.

Comprovação de computador 'explode' equações centenárias de fluidos

Introdução

Durante séculos, os matemáticos procuraram entender e modelar o movimento dos fluidos. As equações que descrevem como as ondulações dobram a superfície de uma lagoa também ajudaram os pesquisadores a prever o clima, projetar aviões melhores e caracterizar como o sangue flui através do sistema circulatório. Essas equações são enganosamente simples quando escritas na linguagem matemática correta. No entanto, suas soluções são tão complexas que entender questões básicas sobre elas pode ser proibitivamente difícil.

Talvez a mais antiga e proeminente dessas equações, formulada por Leonhard Euler há mais de 250 anos, descreva o fluxo de um fluido incompressível ideal: um fluido sem viscosidade ou atrito interno, que não pode ser forçado a um volume menor. “Quase todas as equações de fluidos não lineares são derivadas das equações de Euler”, disse Tarek Elgindi, um matemático da Duke University. “São os primeiros, pode-se dizer.”

No entanto, muito permanece desconhecido sobre as equações de Euler - incluindo se elas são sempre um modelo preciso de fluxo de fluido ideal. Um dos problemas centrais na dinâmica de fluidos é descobrir se as equações falham, gerando valores sem sentido que as tornam incapazes de prever os estados futuros de um fluido.

Os matemáticos há muito suspeitam que existem condições iniciais que causam a quebra das equações. Mas eles não foram capazes de provar isso.

In uma pré-impressão publicado on-line no mês passado, um par de matemáticos mostrou que uma versão específica das equações de Euler às vezes falha. A prova marca um grande avanço – e embora não resolva completamente o problema para a versão mais geral das equações, oferece esperança de que tal solução esteja finalmente ao alcance. “É um resultado incrível”, disse Tristan Buckmaster, um matemático da Universidade de Maryland que não participou do trabalho. “Não há resultados desse tipo na literatura.”

Só há um problema.

A prova de 177 páginas - resultado de um programa de pesquisa de uma década - faz uso significativo de computadores. Isso sem dúvida torna difícil para outros matemáticos verificá-lo. (Na verdade, eles ainda estão no processo de fazê-lo, embora muitos especialistas acreditem que o novo trabalho se mostrará correto.) Isso também os força a considerar questões filosóficas sobre o que é uma “prova” e o que ela fará. significa se a única maneira viável de resolver questões tão importantes daqui para frente é com a ajuda de computadores.

Avistando a Besta

Em princípio, se você conhece a localização e a velocidade de cada partícula em um fluido, as equações de Euler devem ser capazes de prever como o fluido evoluirá o tempo todo. Mas os matemáticos querem saber se esse é realmente o caso. Talvez, em algumas situações, as equações prossigam conforme o esperado, produzindo valores precisos para o estado do fluido em um determinado momento, apenas para um desses valores disparar repentinamente para o infinito. Nesse ponto, diz-se que as equações de Euler dão origem a uma “singularidade” – ou, mais dramaticamente, “explodem”.

Assim que atingirem essa singularidade, as equações não serão mais capazes de calcular o fluxo do fluido. Mas “há alguns anos, o que as pessoas eram capazes de fazer ficava muito, muito longe de [provar a explosão]”, disse Charles Fefferman, um matemático da Universidade de Princeton.

Fica ainda mais complicado se você estiver tentando modelar um fluido com viscosidade (como quase todos os fluidos do mundo real). Um Prêmio do Milênio de um milhão de dólares do Clay Mathematics Institute aguarda qualquer um que possa provar se falhas semelhantes ocorrem nas equações de Navier-Stokes, uma generalização das equações de Euler que explicam a viscosidade.

Em 2013, Thomas Hou, um matemático do California Institute of Technology, e Guo Luo, agora na Universidade Hang Seng de Hong Kong, propôs um cenário em que as equações de Euler levariam a uma singularidade. Eles desenvolveram uma simulação de computador de um fluido em um cilindro cuja metade superior girava no sentido horário, enquanto a metade inferior girava no sentido anti-horário. À medida que executavam a simulação, correntes mais complicadas começaram a subir e descer. Isso, por sua vez, levou a um comportamento estranho ao longo do limite do cilindro onde os fluxos opostos se encontravam. A vorticidade do fluido - uma medida de rotação - cresceu tão rápido que parecia prestes a explodir.

O trabalho de Hou e Luo era sugestivo, mas não uma prova verdadeira. Isso porque é impossível para um computador calcular valores infinitos. Ele pode chegar muito perto de ver uma singularidade, mas não pode realmente alcançá-la – o que significa que a solução pode ser muito precisa, mas ainda é uma aproximação. Sem o respaldo de uma prova matemática, o valor da vorticidade pode parecer estar aumentando até o infinito por causa de algum artefato da simulação. As soluções podem, em vez disso, crescer para números enormes antes de diminuir novamente.

Essas inversões já haviam acontecido antes: uma simulação indicaria que um valor nas equações explodiu, apenas para métodos computacionais mais sofisticados mostrarem o contrário. “Esses problemas são tão delicados que a estrada está repleta de destroços de simulações anteriores”, disse Fefferman. Na verdade, foi assim que Hou começou nessa área: vários de seus resultados anteriores refutaram a formação de singularidades hipotéticas.

Ainda assim, quando ele e Luo publicaram sua solução, a maioria dos matemáticos pensou que era muito provável que fosse uma verdadeira singularidade. “Foi muito meticuloso, muito preciso”, disse Vladimir Sverak, um matemático da Universidade de Minnesota. “Eles realmente fizeram um grande esforço para estabelecer que este é um cenário real.” Trabalho subsequente de Elgindi, Sverak e outros apenas reforçou essa convicção.

Mas uma prova era ilusória. "Você avistou a besta", disse Fefferman. “Então você tenta capturá-lo.” Isso significava mostrar que a solução aproximada que Hou e Luo simularam com tanto cuidado é, em um sentido matemático específico, muito, muito próxima de uma solução exata das equações.

Agora, nove anos após o primeiro avistamento, Hou e seu ex-aluno Jiajie Chen finalmente conseguiram provar a existência dessa singularidade próxima.

A mudança para uma terra auto-semelhante

Hou, posteriormente acompanhado por Chen, aproveitou o fato de que, após uma análise mais detalhada, a solução aproximada de 2013 parecia ter uma estrutura especial. À medida que as equações evoluíram ao longo do tempo, a solução exibiu o que é chamado de padrão autossimilar: sua forma mais tarde parecia muito com a forma anterior, apenas redimensionada de uma maneira específica.

Como resultado, os matemáticos não precisavam tentar olhar para a própria singularidade. Em vez disso, eles poderiam estudá-lo indiretamente, concentrando-se em um ponto anterior no tempo. Ao ampliar essa parte da solução na taxa certa – determinada com base na estrutura autossimilar da solução – eles poderiam modelar o que aconteceria mais tarde, inclusive na própria singularidade.

Demorou alguns anos para eles encontrarem um análogo auto-semelhante ao cenário de explosão de 2013. (No início deste ano, outra equipe de matemáticos, que incluía Buckmaster, usou métodos diferentes para encontre uma solução aproximada semelhante. Atualmente, eles estão usando essa solução para desenvolver uma prova independente da formação de singularidades.)

Com uma solução aproximada auto-semelhante em mãos, Hou e Chen precisavam mostrar que existe uma solução exata nas proximidades. Matematicamente, isso é equivalente a provar que sua solução autossimilar aproximada é estável - mesmo se você a perturbasse levemente e então desenvolvesse as equações começando nesses valores perturbados, não haveria como escapar de uma pequena vizinhança ao redor do solução aproximada. “É como um buraco negro”, disse Hou. “Se você começar com um perfil próximo, será sugado.”

Mas ter uma estratégia geral foi apenas um passo em direção à solução. “Detalhes minuciosos são importantes”, disse Fefferman. À medida que Hou e Chen passaram os próximos anos trabalhando nesses detalhes, eles descobriram que tinham que confiar em computadores mais uma vez - mas desta vez de uma maneira totalmente nova.

Uma Abordagem Híbrida

Um dos primeiros desafios foi descobrir a declaração exata que eles tinham que provar. Eles queriam mostrar que, se pegassem qualquer conjunto de valores próximo de sua solução aproximada e o inserissem nas equações, a saída não seria capaz de se desviar muito. Mas o que significa uma entrada estar “próxima” da solução aproximada? Eles tiveram que especificar isso em uma declaração matemática – mas há muitas maneiras de definir a noção de distância neste contexto. Para que a prova funcionasse, eles precisavam escolher a correta.

“Tem que medir diferentes efeitos físicos”, disse Rafael de la Llave, um matemático do Georgia Institute of Technology. “Portanto, ele precisa ser escolhido usando uma compreensão profunda do problema.”

Depois de descobrirem a maneira correta de descrever a “proximidade”, Hou e Chen tiveram que provar a afirmação, que se resumia a uma complicada desigualdade envolvendo termos das equações redimensionadas e da solução aproximada. Os matemáticos tinham que garantir que os valores de todos esses termos se equilibrassem em algo muito pequeno: se um valor acabasse sendo grande, outros valores teriam que ser negativos ou mantidos sob controle.

“Se você fizer algo um pouco grande demais ou um pouco pequeno demais, tudo se desmorona”, disse Javier Gómez-Serrano, um matemático da Brown University. “Portanto, é um trabalho muito, muito cuidadoso e delicado.”

"É uma luta muito feroz", acrescentou Elgindi.

Para obter os limites rígidos de que precisavam em todos esses termos diferentes, Hou e Chen dividiram a desigualdade em duas partes principais. Eles poderiam cuidar da primeira parte manualmente, com técnicas que incluem uma que remonta ao século 18, quando o matemático francês Gaspard Monge buscava uma maneira ideal de transportar o solo para construir fortificações para o exército de Napoleão. “Coisas como essa já foram feitas antes, mas achei impressionante que [Hou e Chen] as tenham usado para isso”, disse Fefferman.

Isso deixou a segunda parte da desigualdade. Lidar com isso exigiria assistência de computador. Para começar, havia tantos cálculos que precisavam ser feitos, e tanta precisão exigida, que “a quantidade de trabalho que você teria que fazer com lápis e papel seria impressionante”, disse de la Llave. Para balancear vários termos, os matemáticos tiveram que realizar uma série de problemas de otimização que são relativamente fáceis para os computadores, mas extremamente demorados para os humanos. Alguns dos valores também dependiam das quantidades da solução aproximada; como isso foi calculado usando um computador, era mais simples usar também um computador para realizar esses cálculos adicionais.

“Se você tentar fazer algumas dessas estimativas manualmente, provavelmente vai superestimar em algum momento e perder”, disse Gómez-Serrano. “Os números são tão pequenos e apertados… e a margem é incrivelmente pequena.”

Mas como os computadores não podem manipular um número infinito de dígitos, pequenos erros inevitavelmente ocorrem. Hou e Chen tiveram que rastrear cuidadosamente esses erros, para garantir que não interferissem no restante do ato de equilíbrio.

Por fim, eles conseguiram encontrar limites para todos os termos, completando a prova: as equações realmente produziram uma singularidade.

Prova por computador

Permanece em aberto se equações mais complicadas – as equações de Euler sem a presença de um limite cilíndrico e as equações de Navier-Stokes – podem desenvolver uma singularidade. “Mas [este trabalho] pelo menos me dá esperança”, disse Hou. “Vejo um caminho a seguir, uma maneira de talvez até resolver todo o problema do Milênio.”

Enquanto isso, Buckmaster e Gómez-Serrano estão trabalhando em uma prova assistida por computador - uma que eles esperam que seja mais geral e, portanto, capaz de resolver não apenas o problema que Hou e Chen resolveram, mas também dezenas de outros.

Esses esforços marcam uma tendência crescente no campo da dinâmica dos fluidos: o uso de computadores para resolver problemas importantes.

“Em várias áreas diferentes da matemática, está ocorrendo cada vez com mais frequência”, disse Susan Friedlander, um matemático da University of Southern California.

Mas na mecânica dos fluidos, as provas assistidas por computador ainda são uma técnica relativamente nova. Na verdade, quando se trata de afirmações sobre a formação de singularidades, a prova de Hou e Chen é a primeira de seu tipo: as provas anteriores assistidas por computador só foram capazes de lidar com problemas de brinquedo na área.

Tais provas não são tão controversas quanto “uma questão de gosto”, disse Pedro Constantino da Universidade de Princeton. Os matemáticos geralmente concordam que uma prova deve convencer outros matemáticos de que alguma linha de raciocínio está correta. Mas, muitos argumentam, isso também deve melhorar sua compreensão de por que uma determinada afirmação é verdadeira, em vez de simplesmente fornecer a validação de que está correta. “Aprendemos algo fundamentalmente novo ou apenas sabemos a resposta para a pergunta?” disse Elgindi. “Se você vê a matemática como uma arte, então isso não é tão esteticamente agradável.”

“Um computador pode ajudar. É maravilhoso. Isso me dá uma visão. Mas não me dá um entendimento completo”, acrescentou Constantin. “A compreensão vem de nós.”

De sua parte, Elgindi ainda espera elaborar uma prova alternativa de explosão inteiramente à mão. “No geral, estou feliz que isso exista”, disse ele sobre o trabalho de Hou e Chen. “Mas considero mais uma motivação tentar fazer isso de uma maneira menos dependente do computador.”

Outros matemáticos veem os computadores como uma nova ferramenta vital que tornará possível atacar problemas anteriormente intratáveis. “Agora o trabalho não é mais apenas papel e lápis”, disse Chen. “Você tem a opção de usar algo mais poderoso.”

Segundo ele e outros (incluindo Elgindi, apesar de sua preferência pessoal por escrever provas à mão), há uma boa possibilidade de que a única maneira de resolver grandes problemas em dinâmica dos fluidos - ou seja, problemas que envolvem equações cada vez mais complicadas - seja confiar fortemente na assistência do computador. “Parece-me que tentar fazer isso sem fazer uso pesado de provas assistidas por computador é como amarrar uma ou possivelmente duas mãos nas costas”, disse Fefferman.

Se esse for o caso e "você não tem escolha", disse Elgindi, "então as pessoas ... como eu, que diria que isso é abaixo do ideal, devem ficar quietas". Isso também significaria que mais matemáticos precisariam começar a aprender as habilidades necessárias para escrever provas assistidas por computador – algo que esperamos que o trabalho de Hou e Chen inspire. “Acho que muitas pessoas estavam simplesmente esperando que alguém resolvesse esse problema antes de investir seu próprio tempo nessa abordagem”, disse Buckmaster.

Dito isso, quando se trata de debates sobre até que ponto os matemáticos devem confiar nos computadores, “não é que você precise escolher um lado”, disse Gómez-Serrano. “A prova [de Hou e Chen] não funcionaria sem a análise, e a prova não funcionaria sem a ajuda do computador. … Acho que o valor é que as pessoas podem falar os dois idiomas.”

Com isso, de la Llave disse, “há um novo jogo na cidade”.

Carimbo de hora:

Mais de Quantagazine