## How to Read Proofs

Begin by opening up this proof that 4 + 5 = 9. You should see this:

• The proof title is a short description of the proof. Not all proofs have titles.
• The proof name is a unique identifier Ghilbert code uses to reference this particular theorem.
• The edit button allows you to edit the proofs.
• The summary contains a longer description of the proof and how it relates to other theorems.
• The theorem statement describes what the theorem will prove.
• The proof stack contains a step-by-step proof of the theorem.
• The notation guide is there to help you if you don't recognize a symbol or if you'd like more information about it.
• The context guide gives you background about the area of mathematics that this theorem is part of.

## Hypotheses

Sometimes the theorem statement contains multiple lines. The last line of the theorem statement always contains the conclusion to the theorem. The previous lines contain the hypotheses which are starting assumptions that can be used anywhere in the proof. This theorem states that we can cancel a division under the assumption that we are not dividing by 0.

## The Proof Stack

The proof stack contains all the details of the proof. But you do not see all the details at first. The steps of the proof are organized hierarchically starting with a broad overview of the theorem. You can click on a part of the theorem that you are interested in to see more detail on that particular part. When you open up the 4 + 5 proof you will see four statements on the proof stack:

For each of the four equations, there is a short description on the right explaining how that equation was derived. For example, the last step is derived from the "Definition of 9". You can click on any step to see how it was derived. Let's examine how the second step is derived from the first step. Hover over the second step "2 + 7". You will see moving orange arrows which are used to indicate that this step can be expanded. Click on the second step. The proof will expand:

The original first and second steps are still there, but now a new intermediary step has appeared in between them. With this intermediate step, we can derive the equation "4 + 5 = 2 + 7" using a simple substitution. Notice there is now an orange link that says "Substitution". An orange link indicates that we are using a theorem that has already been proven. If you click on the link and it will direct you to the theorem that allows for this substitution. To see how the new intermediary equation "3 + 6 = 2 + 7" was derived, click on it and you will see this:

You see three steps. Click on the first one: "3 + 6 = 2 + 1 + 6" and you will see it was derived from the equation 3 = 2 + 1 which is the definition of 3. Click on 3 = 2 + 1 and you will see this:

As you continue to dig into a proof eventually you reach a point where you get to individual steps of the proof which depend on a definition, axiom, or another theorem. To explore more, click on one of these orange links or try going through another part of the proof.