A system for multi-level mathematical reasoning