Happy tau day, everyone.
Wikiproofs.org is a site where we write math proofs in a formal language which is automatically checked for correctness. We assume axioms and prove theorems from them. Eventually, we hope to prove all of mathematics from a small set of axioms, the axioms of logic and set theory. To get there, we want as many people participating as possible. Our tau day exercises introduce how to write proofs for wikiproofs and provide a (hopefully fun) puzzle for tau day. Warning: Writing formal proofs can be addictive. Don't say we didn't warn you.
The best way to further explain Wikiproofs is by example, and by getting you to start writing some proofs. We have no objection to celebrating tau day in the customary fashion of serving two pies, but this tau day project involves proving some simple statements involving τ. We explain everything you need to know about the mathematics and the proof system, and you should be able to get your first proof written and verified within 6 minutes and 28 seconds (getting to the end may take somewhat longer than that, but not the whole tau day).
To play along, start by editing a proof module. You can create your own account and create a page at User module:YourUsername/Tau day, or you can use the Sandbox. If you get stuck at any point, let us know at WP:TEA. We'd be glad to help, or would love to hear feedback about where it got difficult or boring for you.
The first step
Start by putting the following text into your module:
<jh> import (PROPOSITIONS Interface:Classical_propositional_calculus () ()) import (FIRSTORDER Interface:First-order_logic_with_quantifiability (PROPOSITIONS) ()) import (TAU Interface:Tau_day_axioms (PROPOSITIONS FIRSTORDER) ()) </jh>
Everything between the
<jh>…</jh>-tags is interpreted by the proof verifier. The
jh stands for JHilbert, which is the proof verifier used on Wikiproofs. The import statements tell the verifier to make use of some previously proved, or assumed, results. They provide logic (and, or, implies, etc.) and real numbers which are familiar numbers such as 1, -5, 44/7, √2, τ, or e, as well as operations on real numbers such as addition, division, square root, and a few others.
Once you have copy-pasted those imports into your proof module, hit the preview button. You should see "Proof module parsed successfully" at the bottom of the page in green.
A small exercise
Our first exercise is to show how proofs work by writing a very simple proof. It is just a restatement of something in the tau day axioms file, but with a new name.
Edit the page and move the cursor above the </jh> (everything we will be talking about in this exercise is a formal proof, which means it goes between the <jh> and </jh> tags).
Then we need to declare a variable. So first add
var (real θ) to your proof module, which declares a variable named θ. If your keyboard doesn't have θ, you can insert it by clicking on θ below the edit window. All the variables we will be adding are real numbers, which is what the "real" means.
thm (TauIsPeriodOfSine () (). This indicates we are proving a result called TauIsPeriodOfSine. The empty parentheses are for distinct variable constraints and hypotheses, neither of which we need to worry about for now.
Now we need to state what we are going to be proving. In normal mathemetical notation we'd state it as
sin (θ + τ) = sin θ. Tau (τ) is the ratio of a circle's circumference to its radius. Theta is an angle and sin is the sine function. If you don't remember sine from high school trigonometry, don't worry. One of the nice things about Wikiproofs is that even if you don't have a deep understanding of the concept behind what you are proving, you can still see how each step follows from the previous one. So if you like you can just think of the statements in Interface:Tau day axioms as strings of meaningless symbols, where the rules of the game of assembling them into proofs are given in that file and the others we imported (together with a very simple set of rules built into JHilbert).
Anyway, what we are proving is
sin (θ + τ) = sin θ and we express it almost that way in JHilbert. The main difference is that we need parentheses for everything. So add
((sin (θ + (τ))) = (sin θ)) to your proof.
The actual proof
The only thing remaining is the actual proof. A proof is a set of invocations of existing statements. For this first proof, we just need one invocation, which corresponds to what we are trying to prove. So we will be invoking
SinePeriod (which you can find at Interface:Tau day axioms). To invoke it, we need to notice that
SinePeriod contains one variable:
To invoke a statement, we give expansions for each of the variables which need filling in, in the order in which they occur in the statement, and then the name of the statement. In this example, that is
θ SinePeriod. The entire proof is enclosed in parentheses, so add
(θ SinePeriod) to your proof module. Then add
) (to close out the
That's a completed proof. It should look like this:
var (real θ) thm (TauIsPeriodOfSine () () ((sin (θ + (τ))) = (sin θ)) (θ SinePeriod) )
Hit preview (or save, to save your work back to the wiki), and you should see "Proof module parsed successfully" again. If you get an error, there's a list of error messages near the bottom of Help:JHilbert.
An easy variation on that proof
When we invoke a statement in a proof, we can plug anything in for the expansion of a variable. Your next exercise is to use this fact to prove
sin ((α + τ / 4) + τ) = sin (α + τ / 4) (which is the same as the previous result but with
α + τ / 4 in place of
θ). Call your theorem
TauIsPeriodOfSineQuarterTurn. You will need to declare the variable
α (just as we declared
θ earlier). Come back to this page once you've gotten this new proof to verify.
Statements with hypotheses
The next proof is
sin ((θ + τ / 4) + τ) = sin ((θ + τ) + τ / 4). Set up this proof and call it
CosinePeriodLemma1 (we pick that name because it will eventually help us prove something called
CosinePeriod). The first step in the proof is invoking
Addition23 from Interface:Tau day axioms. Go ahead and write that part of the proof (which gives us
(θ + τ / 4) + τ = (θ + τ) + τ / 4) but leave the parentheses open because the proof isn't finished. After
Addition23 you then write
buildSine. If you look up
buildSine in Interface:Tau day axioms you will see that it takes something of the form
x = y as a hypothesis and gives you
sin x = sin y, which in our case is
sin ((θ + τ / 4) + τ) = sin ((θ + τ) + τ / 4). Fortunately, that is what we need, so close all the parentheses and verify and save this proof.
The proof stack
Our next proof is
sin ((θ + τ / 4) + τ) = cos (θ + τ), which we'll call
CosinePeriodLemma2. The first two steps are to invoke
SineShift, in that order. Look at those two statements and see if you can see what you need to plug in for the variables in each case. When we write two statement invocations after one other, they are put on a proof stack. So then we can invoke something which takes two statements off the proof stack, in this case
applyEqualityTransitivity (which is located in Interface:First-order logic with quantifiability). That's the final step in this proof, so verify and save this proof.
The next theorem to prove is
CosinePeriod, which is
cos (θ + τ) = cos θ. You'll prove it with
SineShift (in that order), together with
applyEqualityTransitivity (both in Interface:First-order logic with quantifiability) to join the pieces together. Figure out what to plug into the variables for each of those theorems, and where you need the
applyEqualityTransitivity. Verify and save that proof.
Cosine of tau
In an effort to keep this exercise to something which could be completed on tau day, we'll make this the last theorem to prove:
cos τ = 1. Prove it using
applyEqualityTransitivity to help. You'll also need
buildCosine which is similar to the
buildSine we saw a few sections ago.
Exporting the result
If you have finished all the exercises to this point, you have proved everything in Interface:Tau day theorems. Add the following to your proof module:
export (THEOREMS Interface:Tau_day_theorems (PROPOSITIONS FIRSTORDER) ())
and verify the page. If the export verifies, it means your proof module has proved all the statements in the Tau day theorems interface. Congratulations!
If you want to keep going, there is another set of exercises at Interface:Tau day theorems 2. They are intended to be done in order, often with each result leading to the next one, but there isn't as detailed a set of instructions as there was for the first set.
- IsarMathLib home page, accessed June 20, 2011
- Gerwin Klein, Slide 3, NICTA Advanced Course: Theorem Proving - Principles, Techniques, Applications, accessed June 20, 2011
- John Harrison (August 13, 1996), Experience of formalized mathematics, accessed June 20, 2011