Terms
agent skill
A folder of instructions and optional resources that an AI agent can load for a particular task.
Its SKILL.md file supplies a name, description and instructions. Scripts, examples and reference files can sit beside it. Narration IR uses this format to guide picture planning and check that quoted text occurs in the cited source.
NVIDIA Auto Ontology
NVIDIA’s framework for describing database concepts and relationships, then using that structure to answer questions with SQL.
The semantic layer connects names and meanings to tables, columns and joins. Code Ontology Bridge supplies a database of Python functions and calls, with descriptions in the format Auto Ontology imports. The framework and Will’s bridge are separate projects.
axiom
A statement assumed without proof inside a formal system.
A theorem can depend on axioms as well as proved results. Lean’s #print axioms command lists those dependencies. Standard mathematical axioms and a placeholder such as sorryAx have different purposes; the dependency list makes that distinction visible.
call graph
A graph of functions and recorded call relations, with an arrow from a caller to the function it calls.
If a calls b, a is the caller and b the callee. Following arrows backwards identifies possible callers affected by a change. A graph built from source text describes the relations its analysis found, which can differ from calls made at runtime.
callback
A function supplied to other code so that code can call it.
In process_items(items, on_item), on_item is passed as a value. process_items may call it immediately, later or repeatedly. Recording this handoff helps a code graph include a relation that a search for direct function calls could miss.
Claude Code hook
A configured action Claude Code runs at a particular event, such as before a tool call.
Hooks can inspect event data and return a decision where the event supports one. Safety Core uses command hooks before selected tool actions to check a retry and, when required, request a person’s approval.
coding agent
An AI application that can use tools to read files, edit code and run commands.
The model proposes actions; the surrounding application runs permitted tools and returns their results. Claude Code and Codex are examples. Agent Trace displays the saved session records produced by those applications.
commit
A recorded snapshot of a project in Git history, with authorship, a message and links to its parent commits.
A normal commit records the prepared index. Most commits have one parent; a first commit has none and a merge can have several. The identifier names that snapshot and its history.
Comparator
A tool that checks a Lean solution against a separately supplied formal challenge statement and permitted axioms.
Comparator compares the relevant formal declarations and checks the proof under its configured conditions. The challenge is itself written in Lean. Matching that challenge is different from comparing the formal statement with the original prose problem.
context compaction
Condensing a long conversation so an AI application can continue within its context limit.
A summary carries forward selected decisions, facts and unfinished work. It can omit detail. Agent Trace lets a user export selected session material into another chat, where it can be summarised before work continues.
Dafny
A programming language and verifier for checking code against written mathematical specifications.
Preconditions describe allowed inputs, postconditions describe required results, and invariants describe what must stay true. Dafny generates proof obligations for these specifications and can compile executable code. Compilation and successful verification are distinct operations.
Lean dependency graph
A graph showing which Lean declarations occur in other declarations’ statements or proofs.
Quartic Reader and General Reader obtain these dependencies from compiled Lean. A node can be a definition or theorem. This graph describes formal use; an authored argument map instead arranges explanatory steps for a reader.
docstring
A string at the start of a Python module, class or function that documents what it does.
Python makes this string available as the object’s __doc__ attribute. CodeMap displays descriptions saved with the code and lets coding agents retrieve them as text. A docstring is documentation, so its accuracy depends on how it is maintained.
DuckDB
A SQL database designed for analytical queries that runs inside the application using it.
A DuckDB database can live in memory or in a file. Code Ontology Bridge stores Python functions and call relations in its tables, then queries those tables directly or through NVIDIA Auto Ontology.
Erdős problem
A mathematical question posed by Paul Erdős, catalogued by number with its known results.
Problem #257 asks whether every infinite selection from 1, 1/3, 1/7, 1/15, … has an irrational sum. The selected terms have the form 1/(2ⁿ − 1). Maths Map brings together work on eight numbered Erdős problems.
EvalPlus
A project for evaluating generated code with expanded test sets, including HumanEval+ and MBPP+.
The expanded tests expose errors that the original benchmark tests can miss. Zenith uses faulty implementations from this setting to score generated test inputs. EvalPlus names the wider project; HumanEval and HumanEval+ name particular benchmarks.
exit code
A number a finished command returns to the program that ran it; zero conventionally signals success.
The meaning of other values depends on the command. A shell pipeline’s reported status can also depend on shell options and which command failed. Reading a test’s recorded output can therefore answer a different question from reading the final exit code.
exposition
An explanation of a mathematical result for readers who do not specialise in that result’s field.
An exposition can introduce the needed ideas, work through examples and then explain the argument. In the funnel it is one of the written outputs between the specialist paper and the video. Its assumed background should be stated for that particular paper.
Flint Hills series
The infinite sum of 1/(n³ sin² n) over positive integers n, with the angle measured in radians.
Some denominators become small when an integer is very close to a multiple of π, linking the convergence question to rational approximations of π. The Atlas example compares reports about an exponent statement and a separate consequence for this series.
forced alignment
Matching a supplied transcript to recorded speech to estimate where its words or sounds occur.
Speech recognition predicts the words; alignment starts from a transcript and estimates their positions in the audio. The boundaries still have uncertainty. A narration plan can use those positions to place visual events near the intended spoken words.
Formal Conjectures
Google DeepMind’s public collection of mathematical problem statements written in Lean.
Its entries include numbered Erdős problems and information about their research and formalisation status. The packet’s #257 example distinguishes the general question from the particular 1968 case linked to Will’s proof repository.
formal verification
Using mathematical methods to establish that a formal model or program satisfies a stated specification.
The specification says what is being checked. A proof may cover one calculation, one theorem or a larger system. Formalising a statement means expressing it precisely; verifying a proof or program is a further task.
Git hook
A script Git can run at a particular stage of an operation, such as before creating a commit.
A pre-commit hook can run checks and stop that commit command by returning a failing status. Other hooks run after an operation. Git hooks belong to Git; Claude Code hooks run at events in the coding-agent application.
Git index
Git’s stored preparation area for the contents of the next commit.
Staging a file or patch updates this area. Later edits in the working tree do not automatically change the staged version. That difference explains how an older staged copy can conflict with another agent’s newly committed fix.
Git patch
A description of changes between file versions, such as added and removed lines with their surrounding context.
Git can produce patch text from a comparison and apply it to another version. One Checkout uses a selected patch to build a commit while leaving other unfinished edits in the shared working tree.
Git worktree
A checked-out working tree with its own Git state, attached to a repository that can also have other worktrees.
Linked worktrees share repository history and objects but have separate checked-out files and index state. They provide separate places to work. One Checkout explores a different arrangement: several agents editing one shared checkout.
ground state
A configuration with the lowest possible energy for the system being considered.
The spin-glass videos use a score equal to minus the energy, so the ground state has the highest score. A near-ground-state configuration has energy close to the minimum; the interesting question is how different such good configurations can be.
held-out problems
Problems set aside from the examples used to develop a method, then used to evaluate it.
In Zenith, the missed-bug material comes from practice problems and the reported comparison uses 58 other problems. Held out refers to this experiment’s preparation; it does not establish that the underlying model never encountered the problems during training.
intermediate representation
A structured form between an input and a final output, used to make a transformation easier to inspect or carry out.
Compilers use intermediate representations between source code and generated code. Narration IR applies the idea to explanation: a plan records sentence meanings, source quotations and visual events before an animation is produced.
irrationality
The property of a real number that cannot be written as p/q for integers p and q with q nonzero.
Every finite sum of fractions is rational, but the limit of infinitely many such partial sums can be irrational. The #257 video proves a particular irrationality result by ruling out every possible denominator using a carefully constructed remainder.
irrationality exponent
A number describing how closely a real number can be approximated by infinitely many fractions.
For x, it is the supremum of exponents μ for which 0 < |x − p/q| < 1/q^μ has infinitely many integer pairs p, q with q positive. A larger exponent permits unusually accurate rational approximations.
Lean 4
A programming language and proof assistant for expressing definitions, statements and proofs that a small kernel can check.
Tactics help construct proof terms; the kernel checks those terms against their types. Files can also contain assumptions or unfinished placeholders, so a successful build alone is not the same as a completed proof of every stated theorem.
Lean proof
A proof expressed in Lean as a term whose type is the theorem statement.
When the kernel accepts the term, it establishes that formal statement from its definitions and declared assumptions. A reader website can link a passage of prose to the declarations involved. Matching the prose to the formal statement is a separate question.
Manim
A family of Python tools for making mathematical animations from code.
Code creates equations, shapes and graphs, then specifies their changes over time. Manim Community and ManimGL are related implementations with different APIs. A narration plan can describe the intended visual explanation before code for a particular renderer is written.
mathlib
The community-maintained Lean library of mathematical definitions and proved results.
A Lean development can import mathlib and build on existing results instead of proving every prerequisite again. Its declarations also appear in dependency graphs and in the list of results a proof uses.
MCP
Model Context Protocol: a standard way for AI applications to connect to tools, data and reusable prompts.
An MCP server can expose executable tools, readable resources and prompt templates. A compatible client decides how to make these available. Agent Trace’s optional server exposes access to saved session records.
nearly quartic separation
A family of problems where randomized query counts grow almost as the fourth power of quantum query counts.
For the relevant total Boolean functions, the construction makes R(fₙ) at least Q(fₙ)^(4 − o(1)) as the family grows: the exponent approaches four. This approaches the known fourth-power upper bound on input queries, rather than total running time.
ontology
A structured account of the kinds of things in a domain, their properties and their relationships.
For code, the kinds might include functions and calls, with relations such as caller and callee. In a database application, these concepts can be connected to concrete tables and columns so a query system has useful context.
Palomar
The formal-proof registry used in the supplied Erdős example to record challenge statements, proof files and checker results.
An entry records the particular submitted statements and proofs alongside its saved results. In the packet’s #257 example, the registry is one route from the paper to the formal statement and the proof that was checked.
PLDI
Programming Language Design and Implementation, an ACM SIGPLAN conference on programming-language research.
General Reader’s current example is Contextual Embeddings, a PLDI 2026 paper. The reader places its text beside the Lean proof released by the paper’s authors.
argument map
An explanatory diagram showing the main steps of an argument and how they connect.
SK Reader’s map was authored from the papers and formal material to help readers follow the explanation. It is different from a Lean dependency graph extracted from compiled declarations. A map can be useful without reproducing every formal dependency.
quantum query complexity
The fewest input-oracle calls a quantum algorithm needs to compute a function with a specified success guarantee.
In the bounded-error setting here, success must be at least two thirds on every input, and the query bound is worst case. A query can act on a superposition of input positions; that does not reveal all those bits separately.
query complexity
The number of calls an algorithm makes to an input oracle, counting those accesses rather than all its computation.
A classical bit query returns a requested input bit. A quantum query is an allowed oracle operation that can act on a superposition. Query complexity compares algorithms in this access model, which is why it is not a direct measurement of elapsed time.
randomized query complexity
The fewest input queries a randomised algorithm needs under a specified success guarantee and query bound.
Here R(f) uses a worst-case query bound and requires a correct answer with probability at least two thirds on every input. The random choices can change which positions are queried. Different conventions should be stated when used.
recursive SQL query
A database query that repeatedly uses rows from an earlier step to find more results.
A recursive common table expression can follow a function’s callers, then their callers, and so on. The query needs a stopping condition or cycle handling appropriate to its form; WITH RECURSIVE by itself does not guarantee termination.
research record
The detailed written account of a result’s reasoning, used as the fuller source for shorter explanations.
In the funnel, the record works through the formal proof and its mathematical context before a specialist paper, exposition and video are produced. It is designed for looking up detail as well as reading sequentially.
semantic model
A description of what data means and how its entities, fields and relationships fit together.
For Code Ontology Bridge, it explains tables of functions and calls, their identifiers and how rows join. This gives a query system more context than column names alone. A semantic layer may also define reusable expressions or measures.
Sherrington–Kirkpatrick model
A spin-glass model in which every pair of spins interacts with a randomly chosen strength.
Each spin is +1 or −1. In a common zero-field convention, H(σ) = −n^(−1/2) Σᵢ<ⱼ Jᵢⱼσᵢσⱼ, with independent standard Gaussian couplings Jᵢⱼ. The videos draw spins as arrows and use a score equal to minus the energy.
specialist paper
A paper written for readers who already know the relevant research field.
It can rely on standard background and concentrate on the result and its argument. In the funnel it is shorter than the research record. The exposition instead supplies more context for readers outside that specialism.
spin glass
A model of a disordered magnet with competing interactions between spins.
A spin can be represented by an up or down arrow. Some interactions favour matching spins and others favour opposite spins, so satisfying one interaction can conflict with satisfying another. The Sherrington–Kirkpatrick model is one particular spin-glass model.
SQL
Structured Query Language: a language for retrieving and changing data organised in relational tables.
A query can select rows, combine tables through joins and compute results. Code Ontology Bridge publishes SQL queries alongside its answers, so the operation can be inspected and rerun against the supplied database.
statement fidelity
How accurately a formal statement expresses the mathematical claim it is meant to represent.
The objects, quantifiers, hypotheses and conclusion all matter. A proof can establish its formal statement even if that statement differs from the paper. Reader links make the two versions easier to compare; the links themselves do not settle the comparison.
static analysis
Examining a program without executing it, using its source code or another representation.
An analysis can extract definitions, calls and possible dependencies. Dynamic dispatch and other runtime behaviour can make these relations incomplete or approximate. Code Ontology Bridge uses source analysis to populate its code database.
test harness
The surrounding code that runs tests, collects results and applies the scoring or pass rules.
A harness can prepare inputs, run a reference implementation and faulty versions, enforce time limits and record outputs. Zenith’s saved responses can be rescored through its harness without generating new model replies.
test input
A value or set of values supplied to a program during a test.
For a function that adds a list, an input might be [2, −1, 0]. A useful input can expose a faulty implementation by producing a wrong result, error or timeout. Not every test input reveals a bug.
text-to-SQL
Turning an ordinary-language database question into an SQL query.
For example, a question about which functions call parse_config can become a query over function and call tables. The system may then run the query and explain the rows. The query’s correctness depends on how well it expresses the question.
timeout
A time limit after which an operation is stopped or recorded as unfinished.
A test harness needs a rule for how to score a timeout. In the Zenith study, timeouts account for roughly half the reported gain. A timeout records that a limit was reached; its cause depends on the program and test setup.
total function
A function defined for every input in its stated domain.
Here the relevant case is a total Boolean function: every n-bit string has an output of 0 or 1. A promise problem restricts the allowed inputs. That distinction matters when comparing randomized and quantum query complexity.
Whisper
OpenAI’s speech-recognition system for turning recorded speech into text.
Its software can also estimate word timestamps. mlx-whisper is an implementation for Apple’s MLX framework; WhisperX is a separate project that adds alignment and other processing around speech transcription. These names are related tools, not synonyms.
word timing
The estimated or annotated start and end positions of spoken words in a particular recording.
A visual event can be attached to a word identifier, then placed in time using the recording’s word positions. Re-recording changes those times, so the event must be aligned with the new audio. Recognition and forced alignment both produce estimates.
working tree
The checked-out files you can read and edit, including changes not yet committed.
The working tree can differ from both the current commit and the index. Saving a file changes the working tree; staging and committing are separate operations. One Checkout leaves other agents’ unfinished edits here while recording a selected patch.