Agent Team

Agents coordinate across collection, informal proof search, and formal verification.

Collector agent illustration

Collector

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

NL Prover agent illustration

NL Prover

An informal 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.