A team, not a chatbot. An orchestrator decomposes a research task and delegates to specialist agents (search, derivation, numerics, review, Lean 4 formalizers), each with its own tools and model. Every claim is grounded in real databases and compiled figures, and every edit lands as a diff you approve.
Three levels of verification 🔗
For work where correctness is non-negotiable, TeXRA connects three layers of checking in one place, with agents that move freely between them.
- 1 LLM prose and equations Fast and creative, but unreliable on algebra.
- 2 Wolfram algebra and numerics Catches sign errors; verifies limits and numerics.
- 3 Lean 4 formal proof Machine-checked. No gaps possible.
What it has produced 🔗
Using this pipeline, a human-guided multi-agent workflow co-designed a Lean-certified catalogue of 14,116 quantum error-correcting codes with prescribed transversal diagonal gates, and resolved transversal-gate problems that had resisted manual search. The work appears in arXiv:2510.20728↗, and the broader case for agents in physics research is in the NeurIPS 2025 position paper arXiv:2506.06214↗.
Model-agnostic, and where to get it 🔗
TeXRA pairs a flagship reasoner for orchestration with cheaper, faster models for routine sub-tasks, and runs against every major provider. It ships as an extension for VS Code, Cursor, and Windsurf, and as a terminal CLI (@texra-ai/cli), published on the VS Code Marketplace, Open VSX, and npm.