Glossary

Short definitions for common terms used in ReasLab and the Lean ecosystem to help new users and improve search discoverability.

Theorem proving

• Using logic and formal rules to construct machine‑checked mathematical proofs.

Interactive theorem prover

• A system where users build proofs step‑by‑step with guidance from the prover and immediate feedback.

Proof assistant

• Software that assists with authoring, checking, and maintaining formal proofs (e.g., Lean 4).

Formal verification

• Proving properties of algorithms or software using mathematical rigor and formal methods.

Formal methods

• Techniques that apply mathematics (logic, specification, verification) to design and validate systems.

Type theory

• A foundational framework for mathematics and programming; Lean uses dependent type theory.

Dependent types

• Types that depend on values, enabling precise specifications and proofs about programs and mathematics.

Tactics

• Scriptable proof steps that transform goals; Lean offers tactic syntax to automate common reasoning.

Goals

• The current statements that remain to be proved in a proof state.

Hypotheses

• Assumptions available in the current proof context that can be referenced to solve goals.

Infoview

• The Lean panel showing goals, hypotheses, messages, and proof state information in real time.