IA e os Problemas Difíceis do Mundo · Ciência da computação teórica · arXiv · 2026-10-22
Autoformalização de longo horizonte de um teorema central subjacente a MIP* = RE
Título original: Long-horizon autoformalization of a core theorem underlying MIP* = RE
Os autores apresentam o FormalFlow, um sistema que coordena agentes de demonstração de IA sob supervisão humana para lidar com a deriva de enunciados e a composição de provas na formalização de longo prazo, usando um blueprint compartilhado para guiar ciclos aninhados de planejamento, demonstração e revisão. Com ele, concluíram, em 63 dias, uma prova em Lean 4 verificada por máquina da solidez quântica do teste clássico de baixo grau individual, um teorema central subjacente a MIP* = RE, com uma biblioteca final de 126,367 linhas de código Lean gerado por agentes. A formalização corrige condições laterais e limites de erro intermediários da prova publicada e melhora o expoente de erro do teorema principal, e o registro do desenvolvimento fornece ferramentas reutilizáveis para verificar matemática de pesquisa em larga escala.