Investigamos o uso de modelos de linguagem de grande escala como assistentes em sistemas de verificação formal de provas matemáticas, com foco em álgebra abstrata. Desenvolvemos um pipeline que combina um verificador formal baseado em Lean 4 com um LLM especializado em raciocínio matemático. Nosso estudo de caso em teoria dos grupos demonstra que o sistema pode verificar e completar provas de teoremas de nível intermediário com 87% de taxa de sucesso, reduzindo significativamente o esforço do matemático humano. Discutimos as limitações atuais e as perspectivas para sistemas híbridos IA-verificação formal.