Use AI to make what AI produces easier to understand, at every level of detail.

Terms used on this page

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.

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.

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.

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.

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.

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.

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.

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.

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.

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.

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.

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.

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.

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.