O Colaborador MáquinaDois Problemas de Erdős · Dois Sentidos de "Resolvido"

Conferido por quem?

A tese deste volume é que um resultado é confiável na medida do que o conferiu — e seu padrão máximo é o cérebro do Lean: zero axiomas além do Mathlib, zero sorry. Em 2026 dois problemas de Erdős, em aberto havia muito tempo, caíram com auxílio de IA. Eles formam um par perfeito, pois se situam em lados opostos exatamente dessa linha: um está resolvido-porque-humanos-brilhantes-o-conferiram, o outro está resolvido-porque-o-cérebro-o-conferiu.

Vencendo a grade — distâncias unitárias

A pergunta de Erdős, de 1946: disponha $n$ pontos no plano; quantos pares podem estar exatamente à distância $1$? Por quase oitenta anos acreditou-se que a grade quadrada era essencialmente ótima. Em maio de 2026, um modelo de raciocínio da OpenAI refutou isso, exibindo uma família infinita de construções — erguidas sobre a teoria algébrica dos números — que atingem $n^{1+\delta}$ pares à distância unitária, uma melhoria polinomial genuína. Will Sawin (Princeton) refinou o expoente para $\delta = 0{,}014$. O argumento foi conferido por Timothy Gowers, Noga Alon e outros; a revisão formal por pares ainda estava em curso.

Conferido pelo cérebro — Erdős #728

O outro resultado de 2026 é o que de fato importa a este volume, pois seu produto é uma prova que uma máquina pode certificar. O Problema #728 de Erdős trata de uma afirmação delicada de divisibilidade fatorial: para quaisquer constantes $0 < C_1 < C_2$ e $0 < \varepsilon < \tfrac12$, existem infinitos triplos $(a,b,n)$ com $\varepsilon n \le a,b \le (1-\varepsilon)n$ tais que $a!\,b! \mid n!\,(a+b-n)!$ e $C_1 \log n < a+b-n < C_2 \log n$.

Foi resolvido por um encadeamento de GPT-5.2 Pro (OpenAI) e Aristotle (Harmonic), operado por Kevin Barreto, e anunciado em 4 de janeiro de 2026 — relatado como o primeiro problema de Erdős considerado plenamente resolvido de forma autônoma por um sistema de IA. Crucialmente, a entrega não foi prosa, mas uma prova em Lean. A estratégia passa pelo teorema de Kummer — que converte a valoração $p$-ádica de uma quantidade do tipo binomial numa contagem de transportes (carries) na adição em base $p$ — e depois por um argumento de contagem que encontra inteiros cujas expansões em base $p$ são "ricas em transportes, mas sem picos", forçando a divisibilidade exigida para todo primo $p \le 2k$.

O enunciado, apresentado de forma ilustrativa em Lean (isto é uma paráfrase do teorema, não a prova de Aristotle — ver arXiv:2601.07421 para o artefato real):

-- Apresentação ILUSTRATIVA apenas do ENUNCIADO. Não é a prova de Aristotle.
-- Fonte de referência: arXiv:2601.07421.
theorem erdos_728 (C₁ C₂ ε : ℝ) (hC : 0 < C₁ ∧ C₁ < C₂) (hε : 0 < ε ∧ ε < 1/2) :
    { t : ℕ × ℕ × ℕ |
        let (a, b, n) := t
        ε * n ≤ a ∧ a ≤ (1 - ε) * n ∧ ε * n ≤ b ∧ b ≤ (1 - ε) * n ∧
        a ! * b ! ∣ n ! * (a + b - n)! ∧
        C₁ * Real.log n < (a + b - n : ℝ) ∧ (a + b - n : ℝ) < C₂ * Real.log n }.Infinite := /- prova de Aristotle -/

Um novo vértice no grafo de Erdős

Erdős media a matemática pela colaboração — o famoso grafo de quem escreveu com quem. O que 2026 acrescenta é um novo tipo de vértice: uma máquina que não apenas auxilia, mas devolve uma prova certificada. É apropriado que o primeiro vértice desse tipo se ligue a um problema de Erdős. O homem que sonhou com "O Livro" — o volume transfinito com as demonstrações mais perfeitas — tem agora provas escritas num livro que uma máquina pode ler e conferir, linha por linha. O retrato do homem está em Vol VII · Erdős; este capítulo é o que sucedeu a seus problemas quando o colaborador deixou de ser humano.

1. Resolution of Erdős Problem #728: a writeup of Aristotle's Lean proof. arXiv:2601.07421. arxiv.org/abs/2601.07421
2. Modelo de raciocínio da OpenAI e o problema das distâncias unitárias no plano (2026); expoente $\delta=0{,}014$ (W. Sawin). Scientific American · TechCrunch
3. Base de dados dos Problemas de Erdős — problema #728 (Bloom). Conferir o enunciado exato contra a base de referência.