TeXRA

An open-source AI theorist for VS Code and the terminal. It attempts real theory work: deriving results, checking derivations in Wolfram, and formalizing proofs in Lean 4. It takes on open problems in long autonomous runs with a team of specialist agents, helping you do good, verifiable work. Manuscript preparation, LaTeX tooling, and figures serve as supporting capabilities within your research project.

entanglement-paper — texra

Launcher Progress

orchestratorGoal4 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. Select 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
Verify proofs and derivations	review, see Built-in agents
Formalize in Lean 4	Lean 4 proofs
Search literature, no fabricated citations	assistant, see Research tools
Tighten prose in a draft	Polish a draft
Fix LaTeX errors and notation	correct agent, see Built-in agents
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
• Multi-agent workflows: how a team lead fans work out to specialists in parallel
• Models: picking a model for the job
• Custom agents: define your own in YAML

Why multi-agent

Theoretical research involves long chains of interdependent steps: a derivation where a subtle sign error in Section 3 invalidates Appendix C; a Lean formalization demanding precise tactic selection to discharge a goal; a numerical simulation that must corroborate an analytical closed form. Alongside the mathematics sits the manuscript itself: notation that must remain uniform from Definition 2.1 onward, every \cite resolving to an authentic citation record, and figures that compile without warnings.

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 check an algebra step, type-check a proof, or diff what changed.
• No tools: no WolframScript, no Mathlib search by type signature, no compiler in the loop.

TeXRA splits 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 underlying agents, credentials, and execution history. A run launched in the CLI surfaces live in the extension's Progress view, and vice versa.

terminal

$texra run polish --input draft.tex

run complete9f3a6c81d24e

executions/9f3a6c81d24e/r1/draft.tex

⇄same run

Progress

polishdraft.tex9f3a6c81d24e

completed — diff ready on r1/draft.tex

One run, two surfaces: the same execution id lands in the terminal's output and the extension's Progress view.

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.

Provider subscriptions (ChatGPT, Grok, Kimi Code, GLM Coding Plan, and GitHub Copilot in VS Code). Requests still go straight from your machine to that provider: ChatGPT and Grok via OAuth sign-in, Kimi Code and the GLM Coding Plan via a plan-specific key. In the VS Code extension the Dashboard → Subscriptions tab can also route models through a GitHub Copilot subscription, with no provider API key needed. Connect one from that tab, or with texra auth chatgpt login / /api in the CLI.

API keys, whichever mode you use, stay on your machine: VS Code's built-in Secret Storage in the extension, an owner-only secrets.json under ~/.texra for the CLI. You can also supply them via environment variables or a .env file in your project (extension only).

Support

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