The Nuprl system is a proof assistant which helps users create formal proofs of theorems. Within the Nuprl language, one defines mathematical objects and then states theorems to prove about these objects. The language which Nuprl uses is typed; that is, every mathematical object is explicitly required to have a type.

In order to prove a theorem which has been entered into Nuprl, the user specifies a sequence of tactics to apply. A tactic is a strategy for proving the current goal given the current hypotheses. The user specifies a tactic to apply and the tactic runs on the current goal and hypotheses to create a set of new subgoals. The subgoals created are labeled as "main", "aux" for auxiliary or "wf" for well-formedness (this is a subset of the "aux" subgoals). Intuitively, auxiliary subgoals prove supplementary facts which are needed for the main branch of the proof to hold and well-formedness subgoals prove that the statements made respect the type information given for the theorem (this is necessary because Nuprl uses a typed language). The user then specifies tactics to use to prove the new subgoals. This process is repeated until every subgoal is proved, in which case the entire theorem is proved.

Nuprl also has objects called conversions which can be used to rewrite clauses or parts of clauses. Conversions are rewrite rules that take a term and rewrite it to an equivalent term. These may be used to manipulate hypotheses to facilitate matching. Once a conversion has been defined, tactics are used to run these conversions and perform the actual rewriting.

The user often knows a sequence of tactics that they wish to apply, such as knowing that once they apply tactic T they want to apply tactic "Auto" to the auxiliary subgoals in order to prove them automatically as they will be simple enough to prove in this manner (this occurs often). Nuprl allows the user to combine the application of tactics, for example by using the "THEN" tactic which takes two tactics as arguments, one to apply first to the current goal and the second to apply to all of the generated subgoals. The only subgoals which are shown are those that remain to be proved after all of the listed tactics are run one the specified subgoals.

Nuprl allows the user to make reference to previously proved theorems, or, as Nuprl refers to them, lemmas. A lemma is invoked by using the name under which the theorem was proved as an argument to a tactic that acts on lemmas. the formal statement of the lemma does not need to be given again. Similarly, mathematical objects such as functions do not need to be defined within a proof but rather are defined outside of proofs and given names. In order to use the definition of such an object, one uses the name under which it was defined as an argument to a relevant tactic.