Dictionary

A model put inside a loop and given tools. You state a goal; it decides which tool to call — run a shell command, read a file, search the web, invoke a proof assistant — reads the result, and repeats until it judges the task finished.

The difference from a chatbot is the feedback: an agent acts, observes what happened, and corrects. That is what lets it carry out "get this Lean file to compile" rather than only describing how you might.

An application programming interface: a way to reach a service from your own code instead of through its web page. For a language model this is normally an HTTPS endpoint you send text to and get text back from, authenticated with a secret key and billed by the token.

The API is what turns a chat window into an instrument — running a model across a thousand conjectures from a script, with the outputs collected in a file you can actually analyze.

A program you drive by typing commands in a terminal rather than clicking in a window — git, lake, python, and most coding agents.

CLIs compose: one program's output becomes the next one's input, and a whole session can be written down as a script and re-run exactly. That reproducibility is why agent tooling has largely settled on the terminal instead of a graphical interface.

The most text a model can attend to at once — your instructions, every document you have given it, the conversation so far, and its own reply, all counted together in tokens.

Anything outside the window may as well not exist. A model is not remembering your earlier session; it is being re-shown it. Windows now run to hundreds of thousands of tokens — a full-length book — but attention thins out across very long inputs, so what you put in still matters more than how much.

A model stating something false with exactly the fluency it uses for the truth: an invented citation, a misattributed theorem, a proof step that reads correctly and is not.

It is not a defect awaiting a patch. The model is producing plausible continuations, and plausibility and correctness come apart — most treacherously in mathematics, where a wrong argument can be locally convincing at every line. This is the case for keeping a proof assistant in the loop: a formalized proof either compiles or it does not.

An open standard for connecting a model to outside tools and data. A server exposes some capability — a database, a computer algebra system, an institute's paper archive — and any MCP-speaking client can drive it.

The point is the once: write the adapter a single time and every compatible agent inherits it, rather than each tool needing bespoke glue for each model.

A function whose parameters were set by training: an architecture that fixes the form, and parameter values fitted to data. The kind you meet first is a large language model (LLM), fitted on a large text corpus to predict what comes next, then tuned to follow instructions. The word covers other trained systems too — diffusion models, world models, and the provers and premise selectors used in formalization. In day-to-day use "the model" also means a released version, named and usually offered in size tiers, as against the product built around it.

A document that interleaves code, prose, typeset mathematics, and the output of running the code — most often a Jupyter notebook, or Colab, Google's hosted version of one. You work in cells and run them one at a time, each result appearing beneath the cell that produced it.

That suits exploration: try a computation, look at the plot, adjust, try again. It works against reproducibility, because cells can be run in any order and saved output need not match the code now above it — the state that produced a figure may no longer exist anywhere. Restart and run from the top before believing a result, or move the settled version into a script you can re-run from a CLI.

The entire input a model processes on one turn — not only the part you typed. Your question and anything you attach to it, but also what the tooling assembles around them: a project's AGENTS.md or CLAUDE.md, the files a skill brings in when the work matches, and the standing instructions the product itself supplies.

So you are usually not looking at the whole prompt, and all of it competes for room in the context window. The parts you do control are worth spending well: say what form you want the answer in, give one worked example, and name the conventions you are working under. What you would otherwise retype every session belongs in the assembled files instead.

A reusable bundle of instructions — sometimes with scripts or reference files alongside — that a model loads on demand when a task calls for it.

Instead of restating your conventions in every prompt, you write them down once ("how we structure a Lean file", "how to prepare the NSF annual report") and the agent picks the bundle up when the work matches. It is procedural memory kept in a folder rather than in a conversation, which means it survives the conversation.

The unit a model reads and writes in: roughly a common word, or a fragment of a rarer one. A page of prose runs to several hundred tokens. Context limits, latency, and price are all quoted in them.

Mathematical notation tokenizes badly — LaTeX macros, unusual symbols, and long identifiers each cost several tokens and arrive as fragments rather than as a symbol. That is part of why models handle discussion of a formula better than manipulation of one.