Zekai Zhu

Numina-Lean-Agent: An Open and General Agentic Reasoning System for Formal Mathematics

Agentic systems have recently become the dominant paradigm for formal theorem proving, achieving strong performance by coordinating multiple models and tools. However, existing approaches often rely on task-specific pipelines and trained formal provers, limiting their flexibility and reproducibility…