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

New task Progress

orchestratorGoal4 turns, 18 tool calls

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.

agent — lean0:24

Agentlean(anthropic/claude-opus-5-5)

InstructionFormalize subadditivity of the von Neumann entropy.

FilesEntropy.lean(input)

% 3 references found · grounded in arXiv

@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 comes from a real lookup — 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 Sessions 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: document tasks vs. chats, 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 work depends on long chains of steps: a sign error in Section 3 breaks Appendix C, a Lean proof needs the right lemma to close a goal, and a numerical script has to match an analytical formula. The manuscript has its own constraints: uniform notation across sections, real citations in BibTeX, and figures that compile cleanly.

General-purpose chatbots struggle with this:

• Hallucinated citations: without grounded search, models invent references.
• Lost structure: a single prompt rarely keeps theorem environments, \label/\ref links, BibTeX, and multi-file projects straight at once.
• No verification: raw text output gives you 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 specialist agents that call real tools and return verifiable output.

Three surfaces, one system

The VS Code extension, the desktop app, and the texra CLI share the same agents, credentials, and run history. A run started in the CLI appears live in the extension's Sessions 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 seen from two surfaces: the same execution id lands in the terminal's output and the extension's Sessions view.

TeXRA's agents run in two ways:

Document tasks

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

polishcorrectmergeocrtranscribe_audiopaper2slidepaper2poster

.tex in → improved .tex + latexdiff

Chat agents

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

researchnumericsreviewleanpresenterlatexFixerlatexDiffcreatorassistantsetup

arXivLeanWolframcompilefilesshell

A document task runs a structured pipeline and returns a diff; a chat works conversationally with grounded tools.

Agents combine three mechanisms: reflection (critiquing and revising their own output), tool use (checking work against compilers, language servers, and search APIs), and planning (breaking a problem into steps and adapting as results come back).

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 and the GLM Coding Plan). 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. ChatGPT and Grok connect from the Settings → Models → Subscriptions tab (or texra auth chatgpt login / /login in the CLI); Kimi Code and the GLM Coding Plan take their key under Models → API keys.

API keys, whichever mode you use, stay on your machine, in one owner-only secrets/ folder under ~/.texra that the extension, the desktop app and the CLI share (readable by your user alone; not keychain-encrypted). You can also supply them via environment variables or a .env file in your project.

Support

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