LAMP: Marco agencial basado en Lean con MCP y Reparación de Pruebas
Los investigadores presentan LAMP, un marco multiagente que sintetiza pruebas verificadas por el kernel de Lean 4 para la Combinatoria sobre Palabras proporcionando conocimiento estructurado del dominio a través de una ontología. Este enfoque aborda la falta de lemas especializados en probadores existentes entrenados principalmente con datos de Mathlib.