Aviso: Eu tinha dado acesso antecipado à versão beta interna do Grok 4.20 Ele encontrou uma nova função de Bellman para um dos problemas em que eu estava trabalhando com meu aluno N. Alpay. O problema se reduz a identificar a função máxima pontual U(p,q) sob duas restrições e entender o comportamento de U(p,0). No nosso artigo, provamos que U(p,0)\geq I(p), onde I(p) é o perfil isoperimétrico gaussiano, I(p) ~ p\sqrt{log(1/p)} quando p ~ 0. Após ~5 minutos, o Grok 4.20 produziu uma fórmula explícita U(p,q) = E \sqrt{q^2+\tau}, onde \tau é o tempo de saída do movimento browniano de (0,1) começando em p. Isso resulta em U(p,0)=E\sqrt{\tau} ~ p log(1/p) quando p ~ 0, uma melhoria de raiz quadrada no fator logarítmico. Alguma importância desse resultado? Não vai te dizer como mudar o mundo amanhã. Em vez disso, dá um pequeno passo em direção à compreensão do que está acontecendo com as médias dos análogos estocásticos das derivadas (variação quadrática) de funções booleanas: quão pequenas podem ser? Mais precisamente, isso dá um limite inferior afiado na norma L1 da função quadrática diádica aplicada a funções indicadoras 1_A de conjuntos A \subset [0,1]. No meu tweet anterior sobre a função de Takagi, vimos que o limite inferior afiado em ||S_1(1_A)||_1 coincide milagrosamente com a função de Takagi de |A| que (surpreendentemente para mim) está relacionada à hipótese de Riemann. Aqui, obtemos um limite inferior afiado em ||S_2(1_A)||_1 dado por E \sqrt{\tau}, onde o movimento browniano começa em |A|. Esta função pertence à família de perfis do tipo isoperimétrico, mas ao contrário da função fractal de Takagi, é suave e não coincide com o perfil isoperimétrico gaussiano. Finalmente, na análise harmônica, é sabido que a função quadrática não é limitada em L^1. A questão aqui era mais sobre curiosidade: como exatamente ela explode quando testada em funções booleanas 1_A. Anteriormente, o melhor limite inferior conhecido era |A|(1-|A|) (Burkholder—Davis—Gandy). No nosso artigo, obtivemos |A| (1-|A|)\sqrt{log(1/(|A|(1-|A|)))}. Esta nova função de Bellman do Grok dá |A| (1-|A|) \log(1/(|A|(1-|A|))) e este limite é realmente afiado.

Se você continuar a testar problemas de Erdős com LLMs, é muito provável que eventualmente resolva um dos problemas em aberto. Os especialistas não estão fazendo isso (por razões óbvias). Os não especialistas assumem que os especialistas estão fazendo. Eles não estão.

Instale o Aristotle. Obtenha a chave da API. Execute-o a partir do seu terminal. Escolha qualquer problema aberto em matemática e insira no aristotle (na sua linguagem natural!). Após várias horas, ele produzirá uma prova formal completa em lean ou poderá falhar. 👏