Using Tex2Lean, step by step.

Opens the connection choices. Select your Claude Code or Codex subscription connection, or an available API provider, and follow its prompts.

Reads the paper and finds statements you can formalize. If several root files are available, choose the main paper. In this example it is esa22-final.tex.

Opens the PDF import workflow when LaTeX sources are unavailable.

Opens this result at its line in the LaTeX editor. Use it to read the source before choosing the result.

Starts formalizing the result on this row: planning the model, writing the Lean statement, and working on its proof.

Starts the workflow from the top of the sidebar. When the paper has several statements, Tex2Lean asks which statement to formalize.

Reads the LaTeX sources again and updates the list after you change your paper.

Finds theorem and lemma declarations already in Model/ and links them to the scanned paper statements. This button does not start proof agents.

Select or deselect results. The counter above the list shows how many are selected.

Starts work on the selected results, one at a time in paper order, within the same Lean project.

Leaves selection mode and returns to the normal result list.

Reopens the model-provider connection choices so you can select a different connection.

Chooses the model used by the connected provider. The available entries depend on your connection; Other… lets you enter a model identifier.

Sets how many agents can work in parallel. Select a number from the row. During a run, changes apply at the next round.

Allows Tex2Lean to answer routine run decisions automatically. With this off, the run stops to ask when it needs your judgment.

Opens the workflow for offering your Lean project to arlib-community through a pull request.

Opens a confirmation listing the generated state that would be deleted for this paper and machine.

Accepts the statement review and starts the proof work.

Holds the run so you can edit the generated Lean statement. When you are ready, use Resume.

Opens the conversation beside your Lean file. You can ask about the statement or type /change followed by the changes you want.

Stops active work and saves a checkpoint. You can continue with Resume.

Opens the formalization maps: paper statements linked to Lean files, and Lean modules linked back to their LaTeX source.

Opens the Tex2Lean output log so you can read the run messages.

Opens a conversation where you can ask about the current proof or suggest what to work on next.

The checked row identifies the theorem the proposal applies to. If several proposals appear, select the statements you want to address. The all and none links select or clear the rows.

Type the statement change you want. For example: “Add the hypothesis n ≥ 2 to the space-bound theorem.” Your text takes priority over the proposal shown in the card. If you leave it blank, Use suggested modification uses the displayed proposal.

Asks an agent to apply your typed change, or the displayed proposal if the box is blank. Tex2Lean checks the edited development, updates the proof tasks, and continues working on the revised statement. If there is no proposal and no typed change, it asks you to supply one.

Stops for you to edit the Lean statement and opens its source file when its location is available. Make your changes in the editor, then press Resume. Text in the box is sent as guidance; this button does not ask an agent to apply it.

Keeps the theorem as written and continues trying to prove it. Any text you entered is treated as proof guidance, rather than permission to change the statement.

Dismisses the proposal and stops this run without authorizing a statement change.

Loads the saved checkpoint and continues the existing formalization.

Opens the maps for exploring the current development.

Opens the conversation beside your Lean file.

Fills the message box with a question about the proof strategy and the work that remains. Review the draft, then send it.

Fills the message box with a question about the assumptions used by the current theorem.

Fills the message box with a question about the next useful step in the formalization.

Type your own question or instructions. Use Shift+Enter to add a new line. During statement review, /change describes the edits you want.

Sends the text in the message box. You can also press Enter.