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 analyse.

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 short 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.

Short for large language model: a neural network with billions of parameters, trained on an enormous text corpus to predict what comes next, then tuned to follow instructions.

"The model" means the trained weights — Claude, GPT, Gemini, Llama — as distinct from the product wrapped around them. Names carry a version and usually a size tier, and behaviour can shift substantially between them. Record which model produced a result; in a year it will be the difference between a reproducible experiment and an anecdote.

A notebook is a document that stores live code, text, math equations, and output inside a single document. It is broken up into cells which can either contain code, text, or output. It is the preferred way to write and execute Python code for a lot of people due to its story-like construction.

Everything handed to the model as input: your question, plus whatever instructions, examples and documents travel with it. A system prompt is the standing instruction framing an entire session.

A prompt is not a command to an interpreter — there is no specification it gets checked against — so phrasing matters more than one would like. The reliably effective moves are the mundane ones: say plainly what you want, show one worked example, state the format you expect back.

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 about 500–800 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.