Agent Team

Agents coordinate across knowledge base management, natural language proof, and formal verification.

KB Manager agent illustration

KB Manager

A persistent research knowledge base. Researchers provide raw sources, and KB-Manager handles reading, extraction, cross-referencing, and compilation into a structured wiki.

NL Prover agent illustration

NL Prover

An natural language proof system with single-agent solve mode and multi-agent orchestration. Sketcher decomposes problems into lemmas, Generators prove them, Verifiers check each proof, and the Orchestrator assembles the final proof.

FL Prover agent illustration

FL Prover

A formal proof system for Lean. It can automatically complete Lean proofs from formalized problems or translate natural-language mathematical arguments into Lean statements and proof scripts.