Resolvendo 20 Problemas de Erdős com 20 Contas do Codex Rodando em Paralelo
Agentes de IA integrados ao Lean 4 e a computação em nuvem em larga escala estão agora gerando provas verificadas por máquina para dezenas de difíceis problemas de Erdős, levantando tanto entusiasmo quanto inquietação sobre o que isso significa para a pesquisa matemática. Os comentaristas investigam a configuração técnica, o financiamento e os planos de código aberto, e observam que, embora as provas formais sejam convincentes, transformá-las em argumentos legíveis e perspicazes para humanos continua sendo um desafio separado. A troca se amplia para questões sobre o valor da matemática pura “inútil”, o futuro papel dos matemáticos humanos à medida que a busca por provas se automatiza e como o teorema automático impulsionado por IA pode eventualmente se ligar ao impacto no mundo real e à mudança econômica.
Infraestrutura, Computação e Acesso ao Modelo
- O projeto usa muitas contas do Codex via tokens OAuth e um broker personalizado que distribui as chamadas da API; “rodando GPT localmente” foi uma questão de formulação, não de auto-hospedar o modelo.
- A computação local é um servidor com múltiplas vCPUs; comentaristas observam que esse hardware é acessível para hobbyistas.
- Agentes de IA têm ferramentas bash e acesso a pacotes matemáticos pré-instalados em VMs.
- Modelos mencionados: GPT-5.6 (para geração), Fable (para verificação/resumos de provas em Lean), embeddings do Gemini.
Harness, Código Aberto e Contribuições
- As perguntas se concentram no “agentic harness”: como os loops são orquestrados, quais modelos “conduzem” e como o progresso é medido; os detalhes continuam em alto nível.
- Outro participante descreve um sistema independente semelhante: inferência soberana na intranet, workers em sandbox para Lean/Sage, modelos de pesos abertos e planos para novo fine-tuning.
- Há interesse em abrir o código do sistema e permitir contribuições; o autor diz que o projeto começou como um experimento rápido e autocontido e pode ser aberto mais tarde.
Validade, Rigor e Textos Explicativos
- As provas em Lean 4 são verificadas por máquina; Fable funciona como uma espécie de árbitro.
- Crítica: os resumos das provas são tecnicamente densos e pouco adequados a leitores humanos; transformar provas formais em explicações claras e esteticamente agradáveis é uma etapa distinta, ainda ausente.
- O autor reconhece isso e planeja melhorar os textos explicativos.
- Algumas soluções de Erdős submetidas foram temporariamente retiradas não por incorreção, mas por enquadramento confuso ou por serem apenas parciais; o trabalho continua.
- Sugestão de integrar a ferramenta “comparator” do Lean para evitar uma sutileza de falta de solidez ao modificar contextos.
Valor da Matemática Pura e do Teorema Automático por IA
- Debate sobre se a matemática pura “inútil” é autocontida e socialmente irrelevante, em oposição à sua história de aplicações inesperadas (por exemplo, criptografia) e ao valor estético intrínseco.
- Alguns veem resolver problemas de Erdős como uma referência e uma fonte de técnicas, não como aplicação direta; o impacto no mundo real pode vir mais de problemas de fronteira ou dos problemas do Milênio.
- Outros argumentam que, mesmo sendo puramente recreativo, isso é tão legítimo quanto qualquer hobby intelectual.
Impacto nos Matemáticos e na Sociedade
- Há preocupações de que sistemas de prova por IA possam “tirar a diversão da matemática” e ameaçar os empregos dos matemáticos; a resposta compara isso a medos anteriores de automação (por exemplo, teares, calculadoras).
- Vários argumentam que os matemáticos passarão a se concentrar em entender, conjecturar e validar provas geradas por IA; provas avançadas já estão frequentemente além da capacidade de uma única pessoa.
- Há também um fio mais amplo sobre desacoplar o sustento do trabalho, uma possível renda básica universal e taxar empresas de IA; há discordância sobre a urgência das mudanças de política.
Estado e Futuro da IA na Matemática
- Muitos expressam espanto pelo fato de LLMs agora conseguirem resolver problemas não triviais de Erdős; a percepção está mudando de “LLMs conseguem fazer matemática?” para “até onde podemos levar isso?”
- Futuro esperado: autoformalização massiva da matemática existente, geração e avaliação automatizadas de conjecturas em grande escala e, possivelmente, esforços distribuídos no estilo BOINC para exploração matemática.