🔢 mathematics

The lonely runner conjecture holds for nine runners

Este artigo prova que a conjectura do corredor solitário é verdadeira para nove corredores ao refinar o método usado anteriormente para estabelecer o resultado para oito corredores.

Autores originais: Matthieu Rosenfeld

Publicado 2026-01-28

📖 5 min de leitura🧠 Leitura aprofundada

CC BY 4.0

Autores originais: Matthieu Rosenfeld

Artigo original sob licença CC BY 4.0 (http://creativecommons.org/licenses/by/4.0/). ✨ Esta é uma explicação gerada por IA do artigo abaixo. Não foi escrita nem endossada pelos autores. Para precisão técnica, consulte o artigo original. Ler aviso legal completo

Imagine uma pista de corrida circular. Nesta pista, há vários corredores, cada um com uma velocidade diferente. Alguns correm rápido, outros correm devagar, e nenhum deles compartilha exatamente a mesma velocidade.

A Conjectura do Corredor Solitário é uma questão matemática sobre esses corredores. Ela pergunta: Existe algum momento no tempo em que todos os corredores estão "solitários"?

Neste contexto, "solitário" significa que cada corredor está longe de todos os outros. Especificamente, se você imaginar a pista como um círculo de circunferência 1, um corredor é solitário se estiver a pelo menos $1/(k+1)$ de distância de todos os outros corredores (onde $k$ é o número de corredores). A conjectura afirma que, não importa como você escolha as velocidades, sempre haverá um momento específico em que isso acontecerá para todos simultaneamente.

Por muito tempo, matemáticos provaram que isso era verdade para grupos de 3, 4, 5, 6, 7 e 8 corredores. Mas para 9 corredores, isso permanecia um mistério.

O Avanço: Resolvendo o Caso de 9 Corredores

Neste artigo, o autor, Matthieu Rosenfeld, prova que a conjectura é, de fato, verdadeira para 9 corredores.

Aqui está como ele fez isso, explicado através de uma analogia simples:

1. O Cenário "Impossível"

Para provar a conjectura, o autor usa um truque lógico clássico: Prova por Contradição.
Ele começa assumindo o oposto: Suponha que exista um grupo de 9 corredores com velocidades específicas onde eles nunca possam estar todos solitários ao mesmo tempo.

Se tal grupo "ruim" de corredores existisse, suas velocidades teriam que ser números muito específicos. O artigo usa uma "cerca" matemática (uma fórmula) para mostrar que, se esse grupo ruim existir, o produto de suas velocidades não pode ser grande demais. Isso estabelece um limite superior para o quão grandes esses números podem ser.

2. O Trabalho de Detetive de "Divisibilidade"

Em seguida, o autor age como um detetive procurando por pistas. Ele pergunta: Se esse grupo "ruim" de corredores existe, por quais números suas velocidades devem ser divisíveis?

Ele usa uma série de regras lógicas (chamadas lemas) para descobrir que as velocidades desses hipotéticos corredores devem ser divisíveis por uma lista muito longa de números específicos (como 17, 19, 23, 29, etc., e até potências de números como 64 e 81).

Pense nisso da seguinte forma: Se você tem um código secreto (o produto das velocidades), o autor prova que esse código deve conter a "chave" para 17, a "chave" para 19, a "chave" para 23, e assim por diante.

3. A Contradição

É aqui que a mágica acontece.

O Limite Superior: A "cerca" do passo 1 diz que o produto total das velocidades deve ser menor que um certo número enorme (vamos chamá-lo de $X$ ).
O Limite Inferior: O "trabalho de detetive" do passo 2 diz que o produto deve ser divisível por uma lista de números tão grande que o produto combinado deles é maior que $X$ .

É como dizer: "Este pote só pode conter 100 bolinhas", mas então provar que "As bolinhas dentro dele devem pesar o suficiente para encher um pote que comporta 200 bolinhas".

Como o produto não pode ser menor que $X$ e maior que $X$ ao mesmo tempo, a suposição inicial deve estar errada. Não existe tal grupo "ruim" de 9 corredores. Portanto, a Conjectura do Corredor Solitário deve ser verdadeira para 9 corredores.

O Papel dos Computadores

Você pode se perguntar: "Como ele verificou todos aqueles números?"
O artigo admite que verificar cada possível combinação de velocidades à mão é impossível. O autor escreveu um programa de computador especializado para realizar o trabalho pesado.

O Problema: O computador tinha que verificar se certos padrões complexos de números poderiam "cobrir" uma pista sem deixar uma lacuna (um espaço "solitário").
A Inovação: O autor não usou apenas resolvedores de computador padrão (que são como usar um martelo para quebrar uma noz). Ele construiu um algoritmo de "backtracking" personalizado e altamente eficiente.
- Imagine tentar encontrar um caminho através de um labirinto. Em vez de percorrer todos os caminhos, seu programa é inteligente o suficiente para perceber: "Se eu virar à esquerda aqui, chegarei a um beco sem saída 10 passos adiante, então nem vou me dar ao trabalho de caminhar até lá".
- Essa otimização fez o computador rodar muito mais rápido do que tentativas anteriores, reduzindo o tempo para problemas semelhantes de 32 horas para 50 minutos.

E Quanto a 10 Corredores?

O artigo menciona brevemente que, embora o método pudesse, teoricamente, funcionar para 10 corredores, a matemática torna-se incrivelmente difícil. A "cerca" fica muito mais alta, e o computador precisaria verificar números tão grandes que levaria um único núcleo de computador cerca de dois anos para concluir o trabalho.

O autor observa que outro pesquisador resolveu independentemente o caso de 10 corredores usando um método de "cribragem" (sieving) ligeiramente diferente e mais rápido, mas este artigo foca estritamente na prova para 9 corredores e nas melhorias específicas feitas na lógica e no código para chegar lá.

Resumo

Em suma, este artigo resolve um enigma de décadas para 9 corredores ao:

Assumir que um grupo "ruim" de corredores existe.
Provar que tal grupo exigiria números que são matematicamente impossíveis (grandes demais para caber no espaço permitido).
Usar um programa de computador personalizado e inteligente para verificar as regras matemáticas que levam a essa contradição.

O resultado confirma que, em qualquer pista com 9 corredores de diferentes velocidades, sempre haverá um momento em que todos estarão perfeitamente sozinhos.

Resumo Técnico: A Conjectura do Corredor Solitário para Nove Corredores

Enunciado do Problema
O artigo aborda a Conjectura do Corredor Solitário (Lonely Runner Conjecture), um problema clássico em aberto na teoria dos números combinatória, proposto pela primeira vez por Wills em 1967. A conjectura postula que, para qualquer inteiro $k \ge 1$ e qualquer conjunto de $k$ inteiros distintos (representando as velocidades dos corredores) $v_1, \dots, v_k$ , existe um tempo real $t$ tal que cada corredor está "solitário". Matematicamente, isso significa que existe um $t$ onde a distância de cada corredor da origem no círculo unitário é pelo menos $1/(k+1)$ , expressa como $\|t v_i\| \ge 1/(k+1)$ para todo $i$ .

Embora a conjectura tenha sido verificada para valores pequenos de $k$ (até $k=7$ ), ela permanece em aberto para o caso geral. Este artigo foca especificamente no caso de nove corredores ( $k=9$ ).

Metodologia
A estratégia de prova baseia-se no trabalho anterior dos autores, que estabeleceu a conjectura para oito corredores. O argumento central baseia-se em uma prova por contradição envolvendo as propriedades de um hipotético "contraexemplo mínimo".

Redução a Restrições de Divisibilidade:
A prova utiliza um limite derivado de Malikiosis, Santos e Schymura (Teorema 1), que implica que, se a conjectura vale para $k$ , ela vale para $k+1$ , desde que o produto das velocidades em qualquer contraexemplo mínimo exceda um limite específico. Consequentemente, para provar a conjectura para $k+1$ , basta mostrar que não existe um conjunto de $k$ velocidades que viole a "propriedade do corredor solitário" (propriedade LR) enquanto satisfaz as restrições de divisibilidade impostas pelo limite.
Lema Generalizado para Divisores:
Os autores introduzem o Lema 6, uma versão fortalecida e generalizada de um lema anterior (Lema 3). Este lema estabelece as condições sob as quais um inteiro $d$ específico deve dividir o produto das velocidades de qualquer conjunto de 8 inteiros que careça da propriedade LR.
- O lema introduz um coeficiente $c$ e considera as velocidades módulo $9cd$.
- Ele incorpora condições de divisibilidade específicas relativas ao número de velocidades divisíveis por 3 e 9 (derivadas do Lema 5).
- A condição requer a verificação de que, para qualquer conjunto de 8 velocidades que satisfaça restrições específicas de MDC e divisibilidade, existe um tempo $t$ que satisfaz a propriedade LR.
Verificação Assistida por Computador (Reformulação de Cobertura de Conjuntos):
Verificar as condições do Lema 6 é computacionalmente intensivo. Os autores reformulam o problema como um problema de cobertura de conjuntos (Lema 7).
- Um inteiro $v$ "cobre" um inteiro $j$ se $\| \frac{jv}{9cd} \| < 1/8$ .
- O objetivo é verificar que não existe um 8-tupla "ruim" que cubra todos os inteiros necessários enquanto satisfaz as restrições de divisibilidade.
- Os autores implementaram um algoritmo de backtracking com otimizações significativas sobre o seu trabalho anterior para $k=7$ $k = 7$ :
  - Bitsets pré-computados para posições cobertas.
  - Estratégias de poda baseadas no número máximo de novos inteiros que um elemento candidato pode cobrir.
  - Memoização para eliminar caminhos de busca redundantes.
- Os autores também testaram abordagens de SAT-solver (usando Cardinality-CDCL e Minicard), mas descobriram que eram significativamente mais lentas do que a sua implementação customizada de backtracking para esta estrutura de problema específica.

Principais Contribuições e Resultados

Prova para Nove Corredores: O artigo fornece uma prova completa de que a Conjectura do Corredor Solitário é válida para $k=9$ .
Identificação de Divisores: Ao aplicar o Lema 6 com um programa de computador, os autores identificaram um conjunto $S$ de inteiros (incluindo potências de primos como $64, 81, 25$ e primos até 191) que devem dividir o produto das velocidades em qualquer contraexemplo mínimo para 9 corredores.
Contradição: O produto dos elementos no conjunto $S$ (que são coprimos entre si) é aproximadamente $9,09 \times 10^{79}$ . No entanto, o limite superior teórico para o produto das velocidades em um contraexemplo mínimo (derivado do Corolário 2) é aproximadamente $8,47 \times 10^{79}$ . Como o produto de divisores exigido excede o produto máximo possível de velocidades, nenhum tal contraexemplo pode existir.
Melhorias Algorítmicas: O artigo detalha melhorias de implementação que reduziram o tempo de execução para o caso de verificação de $k=7$ de 32 horas para 50 minutos, permitindo a verificação mais complexa de $k=9$ .

Significância e Alegações
Os autores afirmam que este resultado estende o alcance conhecido da Conjectura do Corredor Solitário de 7 para 9 corredores. Eles observam que a técnica utilizada é teoricamente aplicável a qualquer número específico de corredores, embora o custo computacional cresça rapidamente.

Independência: Os autores reconhecem que Trakulthongchai anunciou independentemente provas para $k=9$ e $k=10$ pouco antes desta submissão. O trabalho de Trakulthongchai também se baseia na prova de $k=7$ e utiliza uma "abordagem de peneiramento inteligente" que parece ser aproximadamente 100 vezes mais rápida que o método aqui apresentado.
Perspectiva Futura: O artigo discute a viabilidade de estender isso para $k=10$ . Embora o método seja adaptável, estima-se que o custo computacional para verificar primos até aproximadamente 263 levaria dois anos em um único núcleo. Os autores sugerem que combinar as suas melhorias (como considerar potências de pequenos primos) com a abordagem de peneiramento de Trakulthongchai poderia tornar o caso $k=10$ mais tratável, mas não alegam tê-lo resolvido por conta própria.

Em resumo, o artigo resolve com sucesso o caso $k=9$ através de uma combinação de lemas teóricos refinados e verificação computacional altamente otimizada, posicionando modestamente o trabalho como um passo à frente que beneficia e contribui para o esforço mais amplo de resolver a conjectura para números maiores de $k$ .