Research tools
Whether checking an intricate integral against a computer algebra system, tracking down a half-remembered reference from 2017, or importing twenty curated BibTeX entries directly from your Zotero collection, TeXRA's research agents conduct grounded verification and literature search without leaving your workspace.
What you can do
Find papers
Ask a literature-search agent (search, assistant, review, or presenter) to find papers. TeXRA searches arXiv, the web, and your Zotero library:
Find recent papers on transformer architectures for document understanding.
Focus on work from 2023-2024 that handles mathematical equations.User story: A postdoc is writing the related-work section of a NeurIPS submission. She opens the search agent () and asks for papers on "efficient self-attention for long documents." In seconds she has a table of relevant arXiv preprints with titles, authors, and abstracts, ready to cite.
- Longformer: The Long-Document Transformer
- Efficient Attention: Attention with Linear Complexities
- Rethinking Attention with Performers
A typical search result set: each preprint carries its title, authors, an arXiv source tag, and a one-click Cite. Every row is a real lookup, never fabricated.
The same search streams in a terminal, each lookup surfacing as a tool call you can watch:
- ●arxiv_search(efficient self-attention long documents)⎿12 results — "Longformer: The Long-Document Transformer" (arXiv:2004.05150) …
- ●web_search(efficient attention long context)
The postdoc's search in texra chat --agent search: each grounded lookup surfaces as a tool-call row, with results streaming under it.
Download paper sources
For deeper analysis, ask to download the LaTeX source of a paper:
Download the source files for arxiv:2401.12345 so I can see how they made their figures.This uses the download_arxiv_source tool and places the files in your workspace.
Search the web
For documentation, project pages, or general information:
Find the official PyTorch documentation for attention mechanisms.The web_search tool queries the DuckDuckGo Instant Answers API, not a model provider's hosted search. web_fetch retrieves a specific URL and extracts its main content.
Manage references with Zotero
If you use Zotero with the Better BibTeX plugin, TeXRA can search, export, and add items to your library directly. Keep Zotero running while you use these features; check its status and switch it on under Settings → Plugins ().
Search my Zotero library for papers by Vaswani on attention mechanisms.Export the selected Zotero items as a .bib file for my project.Add this arXiv paper to my Zotero library.User story: A PhD student is collecting references for a thesis chapter. She asks the search agent to find key papers on graph neural networks, then says "add these to my Zotero and export them to references.bib." The agent handles the lookup, adds entries to her Zotero library, and writes the BibTeX file, all in one conversation.
- zotero_searchgraph neural networksFinds matching items in your library
- zotero_addarxiv.org/abs/2401.12345Adds the paper to your Zotero library
- zotero_exportreferences.bibWrites the selected items as BibTeX
How the search agent drives the zotero_* tools across one conversation (search → add → export), as the calls surface in the Sessions view.
Default bibliography path
Set a default location for Zotero exports so agents always know where to save bibliography entries. The setting key is texra.bib.defaultPath; configure it in your .texra/config.json.
Verify math with Wolfram
The research agent runs Wolfram Language through wolframscript in the shell (wolframscript -code '...' or wolframscript -file) to check symbolic algebra, integrals, or limits before you commit them to the manuscript. This requires a local Wolfram Engine; its status shows on its Wolfram Language row under Settings → Plugins ().
Formalize proofs in Lean 4
The lean agent formalizes mathematical statements and proofs directly in Lean 4. It searches Mathlib lemmas using Loogle, inspects live proof states and tactic goals, reads compiler diagnostics, and iterates on tactic scripts until the theorem compiles without sorry. Read the Lean 4 proofs guide for full details.
External inquiry
The inquiry tool lets a TeXRA agent ask one question in an external chat (ChatGPT, Claude, Gemini) through a copy/paste flow, then resume with the answer. Dispatch is non-blocking: the agent's cycle continues while you fetch the answer, and resumes automatically once you paste it back (even after a reload). No API key is required; it uses your existing subscription. The inquiry tool is not available in the CLI; there, agents use ask_user_question for synchronous terminal input.
copy outpaste backThe inquiry copy-out / paste-back loop: TeXRA prepares a question, you copy it into ChatGPT, Claude, or Gemini, then paste the reply back to resume the run. No API key needed.
Which agent to use
Specialist research agents are tuned for different stages of the work. Pick one from the Agent dropdown (). search ships with TeXRA and needs no sign-in; the built-in assistant agent carries the same literature toolset (arXiv, web, Zotero). For computational derivations, reach for research; for formal proof verification, use lean:
Finding papers, literature reviews, fact-checking. Built in; the assistant agent has the same tools.
Computational verification with wolframscript in the shell, plus file edits and figure extraction.
Formal proof engineering in Lean 4 and Mathlib with live diagnostic verification.
Each research agent and the tools it has enabled. Check Settings → Agents () for the exact set.
Next steps
- Lean 4 proofs: formalize proofs, inspect goal states, and search Mathlib
- LaTeX tools: formatting, diffs, document statistics, figures, bibliography
- Agent integrations: delegate long-running code tasks to Codex or Claude Code
- Working with figures: feed figures and PDFs to vision models