Há alguns meses, os resultados matemáticos de IA começaram a aparecer em capa de jornal. Naturalmente, me tornei curioso sobre se eu, um novato em matemática, posso encontrar um problema aberto e ter um modelo frontier resolvê-lo. Levou todo um mês de tempo livre e uma quantidade imensa de tokens, mas acredito ter obtido uma prova Lean da conjectura de refinamento de Conway, postada há 50 anos.

A conjectura afirma que se ab = cd, existem inteiros e, f, g, h tais que a = ef, b = gh, c = eg e d = fh. Minha prova não foi verificada independentemente por matemáticos. No entanto, tenho boas razões para acreditar que está correta e realmente convido para refutação.

A prova passou por verificações mecânicas do registro Palomar, e pessoas familiarizadas com Lean e o campo disseram que a afirmação parece correta. Portanto, assumindo que não dependa de um bug no núcleo, é provavelmente legítima. Neste post, descreverei meu abordagem e o que aprendi.

Escolher o campo Peça ao Claude que escolha um problema aberto na programação de pesquisa em números surreais. Os números surreais são uma invenção de John Conway, um sistema numérico contendo todos os números grandes e pequenos: todos os números reais, números ordinais como omega infinitamente grande, e combinações como 75 + omega*3 + 1/omega. O que é maravilhoso é que este sistema rico nasce de uma única regra: gerar um novo número em cada lacuna entre os números já existentes.

Escolher o problema Inicialmente, peço ao Claude por problemas não resolvidos no programa de pesquisa em números surreais.