TeXRA

A LaTeX research assistant for VS Code and the terminal. Multi-agent workflows for writing, reviewing, formalizing, and rendering academic work — with every change returned as a diff you approve.

entanglement-paper — texra

Launcher Progress

orchestratorOdyssey4 turns, 18 tool calls

Todos (2/3)

Ground the literature

Derive the concurrence

Formalize subadditivity in Lean

09:02:11

Survey steady-state entanglement, derive the concurrence, and formalize the entropy bound.

I'll split this across three specialists and assemble their results.

delegate_agent — lean0:24

Agentlean(opus47T)

InstructionFormalize subadditivity of the von Neumann entropy.

FilesEntropy.lean(input)

% 3 references found · DOIs verified via Crossref

@article{wolff2021steady,

title = {Steady-state entanglement in driven spin chains},

author = {Wolff, S. and Kollath, C.},

journal = {Phys. Rev. A}, year = {2021},

doi = {10.1103/PhysRevA.103.022210}

}

Every entry resolves to a real DOI — no fabricated citations. ✓ 3/3 verified

(* concurrence of the steady state, N = 2 *)

rho = SteadyState[lindblad];

C = Concurrence @ rho // FullSimplify

(γ² Sin[2θ]) / (γ² + 4Δ²)

Cross-checked against exact diagonalization at N = 8. ✓ agrees to 1e-9

theorem entropy_subadditive (ρ : State H) :

S (ptrace ρ) ≤ S ρ := by

have h := strong_subadditivity ρ

linarith

⟳ checking proof state · Loogle found 1 lemma

A single task, split across three specialists in the Progress view — click a delegation to see what it produced.

Get started

• Installation — VS Code extension or the texra CLI
• First run — open a .tex file, watch one agent work
• Quick start — the longer walkthrough in VS Code

Use it

Task	Workflow
Tighten prose in a draft	Polish a draft
Fix LaTeX errors and notation	correct agent — see Built-in Agents
Search literature, no fabricated citations	search — see Research Tools
Verify proofs and derivations	review — see Built-in Agents
Formalize in Lean 4	Lean 4 Proofs
Build slides from a paper	paper2slide — see Built-in Agents
Generate TikZ figures	TikZ Figures

Understand the system

• Built-in Agents — the full catalog
• Agent Architecture — workflow vs. tool-use, reflection, planning
• Models — picking a model for the job
• Custom Agents — define your own in YAML

Why multi-agent

The gap between a result and a publishable manuscript is where most research time goes. A 40-page paper where notation must be consistent from Definition 2.1 through Appendix C. A bibliography where every \cite resolves to a real paper. Commutative diagrams that compile. A Lean formalization where the proof state needs careful tactic selection.

General-purpose chatbots make this worse, not better:

• Hallucinated citations — no grounded search means fabricated references.
• Lost structure — one prompt can't reason across theorem environments, \label/\ref graphs, BibTeX, and multi-file projects at once.
• No verification — text output with no way to compile, diff, or type-check what changed.
• No tools — no Mathlib search by type signature, no WolframScript, no TikZ compile.

TeXRA solves this by splitting the work across agents — each specialized, each grounded in real tools, each producing verifiable output.

Two surfaces, one system

The VS Code extension and the texra CLI share the same agents, the same sign-in, and the same run history. A run started in the CLI shows up in the extension's Progress Board, and vice versa.

TeXRA's agents come in two classes:

Workflow agents

Run a structured pipeline → save versioned output files with a diff.

polishcorrectmergeocrtranscribe_audiopaper2slidepaper2poster

.tex in → improved .tex + latexdiff

Tool-use agents

Work conversationally → read & edit files, search, compile, iterate.

researchnumericsreviewleanpresenterlatexFixerlatexDiffcreatorchatsetup

arXivCrossrefLeanWolframcompilefilesshell

Workflow agents run a structured pipeline and return a diff; tool-use agents work conversationally with grounded tools.

The system rests on three established AI design patterns: reflection (agents critique their own output and iterate), tool use (agents ground their reasoning in verified data from compilers, LSPs, and search APIs), and planning (agents decompose tasks, execute steps, and adapt to intermediate results).

Who uses TeXRA

Mathematicians

Complex theorem environments, notation consistency across long proofs, Lean 4 formalization.

Theoretical physicists

Multi-file manuscripts with heavy equation environments, Feynman diagrams, large bibliographies.

Computational scientists

Numerical methods, algorithm descriptions, convergence plots, reproducible workflows.

PhD students

Thesis chapters with consistent notation, literature surveys in new subfields, talks from written work.

Research groups

Collaborations where every change is traceable and auditable by co-authors and referees.

Privacy and data handling

Bring-your-own-key mode. API calls go directly from your machine to the model provider you chose. TeXRA does not sit between you and the provider. Your unpublished proofs, manuscripts, and API keys never leave your machine except to the provider endpoint.

Hosted access (signed in with GitHub or Google). Requests to hosted models are proxied through TeXRA's service so we can manage provider credentials and quota on your behalf. Switch any run back to direct mode with --api-mode personal (CLI) or by adding your own key in the Dashboard → Models tab (VS Code extension).

API keys, whichever mode you use, are stored in your operating system's secure credential store — VS Code's built-in Secret Storage in the extension, the OS keychain (or a local config file) for the CLI. They can also be supplied via environment variables or a .env file in your project.

Support

Issues and feature requests: GitHub. Contact: contact@texra.ai.