Help:Tau day

From Wikiproofs
Jump to: navigation, search

Happy tau day, everyone.[1] 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.[2][3][4] 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.

First proof[edit]

The first step[edit]

Start by putting the following text into your module:

 import (PROPOSITIONS Interface:Classical_propositional_calculus () ())
 import (FIRSTORDER Interface:First-order_logic_with_quantifiability (PROPOSITIONS) ())
 import (TAU Interface:Tau_day_axioms (PROPOSITIONS FIRSTORDER) ())

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[edit]

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.

Next add 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.

geometric explanation for why we might define sine and cosine the way we do

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[edit]

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 thm).

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[edit]

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[edit]

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[edit]

Our next proof is sin ((θ + τ / 4) + τ) = cos (θ + τ), which we'll call CosinePeriodLemma2. The first two steps are to invoke CosinePeriodLemma1 and 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.

Cosine period[edit]

The next theorem to prove is CosinePeriod, which is cos (θ + τ) = cos θ. You'll prove it with CosinePeriodLemma2, SinePeriod, and SineShift (in that order), together with swapEquality and 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 swapEquality and applyEqualityTransitivity. Verify and save that proof.

Cosine of tau[edit]

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 AdditiveIdentityLeft, CosinePeriod, and Cosine0, with swapEquality and applyEqualityTransitivity to help. You'll also need buildCosine which is similar to the buildSine we saw a few sections ago.

Exporting the result[edit]

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!

Theorems 2[edit]

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.

What next?[edit]

You can find another example explaining how to write proofs at Help:Tutorial. To find things to contribute to, browse Category:Pages needing cleanup. Feel free to ask questions at WP:TEA.


  2. IsarMathLib home page, accessed June 20, 2011
  3. Gerwin Klein, Slide 3, NICTA Advanced Course: Theorem Proving - Principles, Techniques, Applications, accessed June 20, 2011
  4. John Harrison (August 13, 1996), Experience of formalized mathematics, accessed June 20, 2011