ProofScript Programming Language

How Proof Works in ProofScript

A proof is not a comment, a test result, or a Boolean that happened to return true. It is checked evidence for an exact proposition.

Home · Docs · Type Theory · Proofs · Verified Software · ProofScript → Lean + TypeScript · Reference · Examples · Download

This page starts with one tiny theorem and gradually opens the machinery underneath it. If you have never used a theorem prover, read the English translations before worrying about the formal names.

Syntax note: canonical definitions use def; beginner examples may use the function/top-level const aliases. The theorem and proof semantics are unchanged.

1. A theorem is a typed declaration

Start here:

theorem twoPlusTwo: 2 + 2 = 4 := by {
  rfl
}

In English

“Declare a theorem named twoPlusTwo. Its proposition is that 2 + 2 equals 4. Provide a proof by showing that both sides reduce to the same value.”

Every piece of syntax

Part Meaning
theorem introduce a named proved proposition
twoPlusTwo theorem name
: “has the following type”
2 + 2 = 4 proposition being proved
:= provide the theorem’s value/proof
by begin tactic-style proof construction
rfl close equality by reflexivity after definitional computation

The important fact is:

twoPlusTwo : 2 + 2 = 4

The theorem name is not the guarantee. The theorem’s type is the guarantee.

2. Why a proposition can be a type

From Type Theory:

2 + 2 = 4 : Prop

The equality statement is a value of universe Prop: a proposition.

A proof of that statement has the proposition as its type:

proof : 2 + 2 = 4

So a theorem declaration can be understood like a definition whose declared type happens to be a proposition.

The key pattern is:

ordinary definition
name : DataType := dataValue

proof definition
theoremName : Proposition := proofValue

This is one reason := is so natural in theorem syntax: it is literally providing a term of the claimed type.

2A. The first mental model: a theorem is a function waiting for evidence

Before tactics, imagine this ordinary function:

function keepValue{A: Type}(x: A): A := {
  x
}

It receives an A and returns an A.

Now replace the ordinary type A with a proposition P:

P → P

Read:

“Given a proof of P, return a proof of P.”

That is also the logical statement:

“If P is true, then P is true.”

A tactic proof such as:

theorem keep(P: Prop): P → P := by {
  intro h
  exact h
}

is therefore constructing something very much like the identity function on proof evidence.

This propositions-as-types reading is central in Lean. Official background: Theorem Proving in Lean 4 — Propositions and Proofs and Lean Language Reference — Propositions.

3. What rfl actually does

rfl is short for reflexivity.

Mathematically, every value is equal to itself:

x = x

But theorem provers also have definitional equality: expressions may count as the same because they compute/unfold to the same core expression.

Consider:

function double(n: Nat): Nat := {
  n + n
}

Then:

theorem doubleTwo: double(2) = 4 := by {
  rfl
}

A simplified computation story is:

double(2)
→ 2 + 2
→ 4

So after reduction, the goal is essentially:

4 = 4

and reflexivity closes it.

rfl is therefore a beautiful first example of the interaction between computation and proof.

4. Proof state: assumptions above, goal below

Interactive theorem provers often show a proof state conceptually like:

n : Nat
────────────
n = n

Read it as:

“We have an arbitrary natural number n. Our current goal is to prove n = n.”

For a more complex context:

a   : Nat
b   : Nat
hab : a < b
────────────
a + 1 ≤ b

The lines above the divider are the local context: values and assumptions currently available.

The line below is the goal.

A tactic transforms one proof state into zero or more new proof states while constructing evidence.

The proof is finished when no goals remain and the constructed term passes final checking.

5. exact: use the evidence you already have

theorem keep(P: Prop, h: P): P := by {
  exact h
}

In English

“Given a proposition P and a proof h of P, prove P by returning exactly that proof.”

Before exact h:

P : Prop
h : P
────────
P

The goal asks for a value of type P. h already has exactly that type.

So:

exact h

means:

“Use h; it exactly matches the goal.”

This is not search or magic. It is ordinary typed value use.

6. intro: proving implication by writing a function

Suppose the goal is:

P → P

Under propositions-as-types, that is a function type.

To construct a function, introduce its input:

theorem identityImplication(P: Prop): P → P := by {
  intro h
  exact h
}

After intro h, the proof state becomes:

P : Prop
h : P
────────
P

Then exact h finishes.

What happened logically?

You proved:

“If P holds, then P holds.”

What happened computationally?

You constructed the identity function on proof values:

fun h => h

This is Curry–Howard in action without any mystical step: proving implication is constructing a function.

7. assumption: find a matching local proof

This proof:

theorem identityImplication2(P: Prop): P → P := by {
  intro h
  assumption
}

means the same idea.

assumption searches the local context for an available value whose type matches the goal.

It does not invent a theorem. It reuses evidence already present.

8. Universal theorems are functions over arbitrary values

theorem successorGreater(n: Nat): n < n + 1 := by {
  omega
}

Read:

“For any natural number n, prove that n is smaller than n + 1.”

The theorem does not test several examples such as 0, 1, 2, and 10_000.

The parameter n is arbitrary. The proof establishes the proposition for every n in the theorem’s domain.

Conceptually the theorem has the dependent function type:

(n: Nat) → n < n + 1

That is universal quantification expressed as a function that returns proofs.

9. omega: automation is still proof construction

In:

theorem successorGreater(n: Nat): n < n + 1 := by {
  omega
}

omega is an arithmetic decision procedure/tactic for a supported fragment of arithmetic.

A beginner can read it as:

“Use arithmetic reasoning to construct evidence that this goal follows.”

The important trust model is not:

omega says true
→ accept theorem

It is conceptually:

arithmetic goal
      ↓
omega reasoning
      ↓
proof evidence / checked result
      ↓
core checker

Proof automation can be sophisticated while the final logical acceptance criterion remains strict.

10. rw: equality lets you replace equals by equals

Suppose:

h : a = b

and your goal contains a.

Then:

rw [h]

means:

“Rewrite using the equality proof h.”

Example:

theorem replaceEquals(a: Nat, b: Nat, h: a = b):
    a + 1 = b + 1 := by {
  rw [h]
}

In English

“If a equals b, then adding one to each gives equal results.”

The equality proof justifies substitution.

This is propositional rewriting, not text replacement.

11. simp: proof-producing simplification

Many theorems reduce through common identities and registered simplification lemmas.

theorem addZero(n: Nat): n + 0 = n := by {
  simp
}

Read:

“Simplify the goal using definitions and trusted/proved simplification rules until the result closes.”

The important point is that simp is not merely a pretty-printer. It is part of proof construction and must justify its rewrites.

Use rw when you want an explicit rewrite sequence. Use simp when a normalization-oriented collection of simplification rules is appropriate.

12. cases: prove by exhausting constructors

Suppose x: Option(A).

There are two constructors conceptually:

none
some(a)

A proof by cases x splits the theorem into the possible ways x could have been built.

Example from the ProofScript reference style:

theorem optionCases{A: Type}(x: Option(A)):
    x.isSome = true ∨ x = .none := by {
  cases x with
  | none =>
      exact Or.inr(rfl)
  | some a =>
      exact Or.inl(rfl)
}

Read the proposition first

x.isSome = true ∨ x = .none

∨ is logical “or.”

So the theorem says:

“For any option x, either its isSome proposition holds as stated here or x is none.”

Then cases x handles the none and some constructors separately.

The proof structure follows the data structure.

13. induction: cases plus an induction hypothesis

For recursive data such as lists, proving a property for all lists often needs a stronger principle than simple case analysis.

Suppose a list is either:

[]

or:

x :: xs

For the second case, induction gives you an extra assumption: the theorem is already known for the smaller xs.

That assumption is the induction hypothesis.

Conceptually:

Base:
prove P([])

Step:
assume P(xs)
prove P(x :: xs)

The reason this is valid comes from the inductive structure of lists.

14. A worked induction idea: length of append

Suppose append has the usual list semantics and we want:

length(append(xs, ys)) = length(xs) + length(ys)

A proof by induction on xs follows the list constructors.

Base case

xs = [].

Then:

append([], ys) = ys

so the theorem reduces to:

length(ys) = 0 + length(ys)

which simplifies.

Step case

xs = x :: rest.

Assume the induction hypothesis:

length(append(rest, ys))
=
length(rest) + length(ys)

Then unfold append and length for x :: rest, rewrite using the induction hypothesis, and simplify arithmetic.

The proof is finite because the inductive rule lets one assumption stand for the already-proved property of the smaller recursive part.

15. Why induction is not “testing all lists”

There are infinitely many lists.

Induction does not enumerate them.

It uses the fact that every finite list is generated by a finite number of applications of the constructors.

If:

  1. the property holds for the base constructor, and
  2. whenever it holds for the recursive component it also holds after one constructor step,

then it holds for every value generated by the inductive definition.

This is a structural argument, not exhaustive testing.

16. Proof term versus tactic proof

Tactics are a convenient way to construct proof terms.

For a simple implication:

theorem keep(P: Prop): P → P := by {
  intro h
  exact h
}

The underlying idea is equivalent to a direct function term:

fun h => h

The tactic view says:

1. introduce the premise
2. solve the goal with the premise

The term view says:

return the argument

Both inhabit the same proposition type.

Learning both views is valuable:

17. Proof construction versus proof checking

This distinction is central to trust.

Proof construction may use

Final logical checking asks

Does the explicit resulting declaration/term satisfy the core type theory?

Lean deliberately keeps its trusted kernel smaller than the rich source language. The official Lean reference describes parsing, macro expansion, elaboration, kernel checking, and compilation as separate concerns.

The ideal trust shape is:

powerful producer
      ↓
explicit evidence
      ↓
small strict checker

This is much easier to trust than making every tactic and search heuristic part of the logical foundation.

18. A theorem can be valid but useless

Formal validity is not the same as useful specification.

Suppose your “sort correctness” theorem says only:

Ordered(sort(xs))

A broken implementation:

sort(xs) = []

could still produce an ordered list.

So you also want something like:

Permutation(xs, sort(xs))

Now you know:

This is the specification problem: the checker proves exactly what you asked, not what you meant but forgot to state.

19. Preconditions can make theorems vacuously true

Consider a theorem:

P → Q

If P can never hold, the implication is logically easy to prove—but perhaps useless for the intended software domain.

The same risk appears in contracts.

A function can have a postcondition that is correct only under an impossible precondition.

So high-quality formal verification asks two questions:

  1. Is the theorem valid under the stated assumptions?
  2. Are the assumptions meaningful and satisfiable for the intended use?

These are different proof obligations.

20. Axioms change the assurance profile

An axiom introduces a proposition/value without proving it from the current theory.

That can be legitimate: formal developments sometimes state assumptions intentionally.

But a theorem depending on an axiom is conditional on that assumption.

A mature verification report should therefore expose transitive assumptions rather than presenting every accepted theorem as equally assumption-free.

Think:

theorem
+
assumption manifest

not merely:

green checkmark

21. sorry is not proof

During development, proof assistants may support placeholders such as sorry for incomplete work.

A strict verified artifact must not silently treat unresolved placeholders as completed proof evidence.

For production assurance, the verification profile should report and reject unapproved sorry dependencies.

The principle is simple:

A placeholder is useful for editing. It is not a finished proof.

22. Native or trusted computation needs explicit accounting

Some proof procedures can rely on computation outside the smallest kernel reduction path for performance.

That does not make them automatically bad, but it changes the trusted computing base.

A serious verifier records which assumptions or native-computation mechanisms a theorem transitively relies upon.

The question is not:

“Was automation used?”

The better question is:

“What evidence and trusted mechanisms does the final theorem depend on?”

22A. When a proof fails, read the goal before reaching for automation

Beginners often respond to a failed proof by trying more tactics. A better debugging habit is:

1. Read the goal in English.
2. Read every local assumption in English.
3. Check whether the statement is actually true.
4. Check whether an assumption you need is missing.
5. Only then choose a tactic.

Suppose the goal is:

n : Nat
────────────
n - 1 < n

This is not true for all n : Nat, because n = 0 gives 0 - 1 = 0 in natural-number subtraction, so the goal becomes 0 < 0.

The missing idea is a precondition:

h : 0 < n

Then the intended theorem becomes:

theorem predLess(n: Nat, h: 0 < n): n - 1 < n := by {
  omega
}

This is an important lesson in formal verification: a failed proof is often not “the prover being difficult.” It may be exposing an underspecified or false requirement.

23. Inspect the theorem type

Before celebrating a proof, inspect what was actually proved.

Conceptually, a verification tool should let you answer:

What is the exact theorem type?
What definitions does it reference?
What assumptions does it depend on?
Which source artifact produced it?
Which toolchain checked it?

This matters because a frontend can, in principle, emit a perfectly valid proof of the wrong proposition.

Kernel validity answers:

“Is this elaborated proposition proved?”

Source/specification fidelity asks:

“Is this the proposition the source and user intended?”

24. Statement binding: prove the right theorem

Imagine a challenge asks you to prove:

secureTransferPreservesBalanceInvariant

but a buggy translator emits and proves:

1 + 1 = 2

The kernel is correct to accept 1 + 1 = 2.

But the workflow failed.

Therefore high assurance must bind:

source identity
+
exact theorem statement
+
definition/environment identity
+
assumptions
+
checker/toolchain

Proof replay alone is not enough if the replayed theorem is not the intended theorem.

25. Independent checking

Explicit proof terms/declarations allow another checker to replay the logical claim.

For Lean-compatible artifacts, a high-assurance workflow can include:

ProofScript source
      ↓
generated Lean artifact
      ↓
Lean kernel replay
      ↓
optional independent checker

This reduces some classes of implementation risk.

It does not prove that all checkers are bug-free or that source-to-Lean translation was correct. Multiple implementations provide diversity, not metaphysical certainty.

Lean’s own high-assurance validation story is layered

Lean’s official documentation has a dedicated guide to validating proofs. High-assurance workflows distinguish ordinary checking from assumption inspection, environment replay, and stronger external/comparator workflows. This supports the ProofScript rule that “the kernel accepted a proof” and “this source artifact proves exactly the claim we intended” are related but distinct assurance questions.

Official background: Lean Language Reference — Validating a Lean Proof.

26. Proof does not automatically reach generated TypeScript

Suppose you have proved:

normalize(normalize(x)) = normalize(x)

about the checked ProofScript definition.

If a buggy TypeScript emitter accidentally outputs:

normalize(x) = randomValue()

then the source theorem remains valid while the executable translation is wrong.

That is why executable correctness needs a compiler/execution correspondence claim in addition to source-level theorem checking.

The verified chain is conceptually:

source theorem
      ↓
logical validity

source program
      ↓
semantic-preserving translation
      ↓
TypeScript program

Two different questions. Two different kinds of evidence.

Read ProofScript → Lean + TypeScript.

27. Proof also does not automatically model the world

Even perfectly generated TypeScript eventually touches things outside pure mathematics:

A theorem can cover those only to the extent that their behavior is included in the formal model and the runtime correspondence assumptions are justified.

This is why real software assurance is layered.

28. Where proof is strongest

Proof gives especially strong leverage where you can write a clear mathematical model of a high-value invariant.

Examples:

Pure transformations

normalize(normalize(x)) = normalize(x)

Data-structure relationships

length(append(xs, ys)) = length(xs) + length(ys)

Bounds

i : Fin(xs.size)

Round trips

decode(encode(x)) = some(x)

State transitions

Invariant(s) → ValidTransition(s, s') → Invariant(s')

Authorization refinement

authorize(u, a) = allowed → PolicyPermits(u, a)

These statements can cover entire mathematical domains rather than a finite test suite.

29. Tests and proofs answer different questions

A test says:

“For this selected input and environment, I observed this result.”

A theorem says:

“For every value covered by these quantified variables and assumptions, this formal proposition follows.”

But tests can inspect aspects a theorem model may not cover:

So the right relationship is:

proofs + tests + review + runtime validation

not:

proofs replace all engineering

30. A complete mental model of proof

When you see:

theorem T(args...): P := by {
  tactics...
}

read it as:

1. `P` is a proposition/type.
2. The theorem parameters define arbitrary inputs and assumptions.
3. The tactic script tries to construct a term of type `P`.
4. The checker validates the resulting term/declaration.
5. If accepted, `T` is evidence for exactly `P` under exactly those assumptions.
6. The theorem says nothing automatically about properties not contained in `P`.
7. Connecting `P` to generated TypeScript execution requires separate correspondence evidence.

That is how ProofScript proves things.

Sources

Next: Verified Software →