Home / What is a proof?

What is a proof?

You already know what a proof is, loosely. "I can prove the earth is round" means you have evidence and arguments that would convince a reasonable person. That's fine for everyday life.

Mathematical proof is different. It's not about evidence, experiments, or persuasion. A proof is a chain of logical steps where each step follows from the previous ones by a clear, agreed-upon rule. Nothing more. If the rules are valid and you followed them correctly, the conclusion is guaranteed to be true. No wiggle room, no exceptions, no "well, actually."

Here's one you already understand:

1. If it's raining, the ground is wet.
2. It's raining.
3. Therefore, the ground is wet.

That's it. You just used a rule of logic called modus ponens: if you know P → Q (P implies Q) and you know P, then you can conclude Q. Formal proof is just being very precise about which rules you're using at each step.

Why bother being formal?

Three reasons:

1. Certainty. A formal proof cannot be wrong (if the rules are sound). Unlike empirical science, it doesn't need replication or peer review to be trusted. The logic itself is the guarantee.
2. Computers can check it. Programs like Lean, Coq, and Agda verify proofs mechanically. If it compiles, it's correct. No human error, no hand-waving, no "the proof is left as an exercise."
3. Understanding. Writing a proof forces you to understand exactly why something is true, not just that it is. You can't hide behind intuition.

What does a proof look like?

Let's see the same modus ponens proof in three notations, from informal to fully formal.

1. English

If it's raining then the ground is wet. It's raining. Therefore the ground is wet.

Clear, but imprecise. Which rule did we use? What exactly are the premises? A reader has to figure that out themselves.

2. Gentzen-style natural deduction

This is the notation we start with on this site. Premises go on top, the conclusion goes below a horizontal bar, and the rule name sits on the right:

  P      P → Q
————————————————  →-Elim
       Q

Read it as: "Given P and P → Q, we may conclude Q by the rule of implication elimination." Every step names its rule. Nothing is implicit.

3. In Lean 4

This is what we'll work up to. Lean is a programming language and proof assistant. Here's the same proof:

theorem ground_wet (raining : P) (rain_means_wet : P → Q) : Q := by
  exact rain_means_wet raining

The exact tactic tells Lean: "apply rain_means_wet to raining and that gives us Q." Lean checks this mechanically. If there's an error in the logic, it won't compile.

Don't worry if the Lean syntax looks alien. You'll get there. The point is that all three notations express the same logical step.

Where to start

Pick the path that fits your background:

• I've never seen any of this before. Start with the Proof Theory track. It introduces the rules of logic one at a time, with no programming required.
• I know basic logic but not Lean. Start with the Logic track. It translates what you already know into Lean 4 proofs.
• I've used a theorem prover before. Jump straight to Strategies for proof techniques like contradiction, induction, and case analysis.