Agents that search, derive, calculate, compile, and verify — built for work where correctness is non-negotiable.
The research agent builds the Lindblad superoperator, solves for the steady state in Wolfram, computes the concurrence analytically, and cross-checks with exact diagonalization in Julia at N=8.
The correct agent unifies notation — \lambda_2 vs \mu for the same eigenvalue across sections — fixes label conflicts, and outputs a diff you review line by line.
The lean agent searches Loogle for the right Mathlib lemma, reads the proof state, adds a missing hypothesis, and produces a proof that compiles with zero errors.
Install from the VS Code Marketplace, add an API key, and run your first agent.
Claude, GPT, Gemini, DeepSeek, Grok, and more via OpenRouter. Bring your own API key, or sign in for free researcher access.
Yes — via git sync. See the Overleaf guide.
Yes — Loogle search, proof state inspection, diagnostics, build and cache management. Requires the Lean 4 extension.
All API calls go directly from your machine to the model provider. No TeXRA servers in the middle.
Yes — agents are YAML files you can modify or create from scratch. See Custom Agents.
Email contact@texra.ai or open an issue on GitHub.
