LAMP: Легковесная агентная платформа на основе MCP и восстановления доказательств
Исследователи представляют LAMP, многоагентную платформу, которая синтезирует проверяемые в ядре доказательства Lean 4 для Комбинаторики на словах, предоставляя структурированные предметные знания через онтологию. Этот подход решает проблему отсутствия специализированных лемм в существующих доказывателях, обученных преимущественно на данных Mathlib.