A coordinated research environment in which a knowledge-base manager, natural-language prover, and formal-language prover form a closed loop for discovery, proof development, and Lean verification.
- Shared mathematical memory and evidence tracking
- Multi-agent exploration and proof development
- Formal certification in Lean 4
