The EPGY Theorem Proving Environment

Sample Proofs

We have collected movies depicting several proofs. Some were recorded as they were actually being constructed, others we reconstructed from submitted students' proofs.

An expert's proof that two vectors in R² are parallel if and only if a certain algebraic formula hold:

m52aPARALLEL.avi (5,751KB)

An expert's proof that eigenvectors with distinct eigenvalues are linearly independent:

m51aEIGENVECTOR.avi (3,820KB)

A student's proof that a square matrix can be decomposed into the sum of a symmetric and a skew-symmetric matrix:

ex46student.avi (4,362KB; narrated by a course author)

An expert's proof that a square matrix can be decomposed into the sum of a symmetric and a skew-symmetric matrix:

ex46expert.avi (3,115KB; narrated live during the proof, with editing to show the EPGY Derivation System)

A student's proof that matrix inverses are unique:

ex41student.avi (1,010KB; narrated by a course author)

An expert's proof that matrix inverses are unique:

ex41expert.avi (599KB; no narration, but edited to show the EPGY Derivation System)

A student's proof that if S and T are invertible matrices, then ST is invertible and (ST)^-1 = T^-1S^-1:

ex42student.avi (2,477KB; narrated by a course author)

A student's proof that tr(AB) = tr(BA) for matrices A and B:

ex34student.avi (narrated by a course author)

A student's proof that, if A is an invertible matrix, then tr(A) = tr(ABA^-1):

ex35student.avi (1,278KB; narrated by a course author)

A demonstration of the proof that (AB)^T = B^TA^T for matrices A and B:

ex33expert.avi (998KB; no voice)

To view a movie, we recommend that you download it and play it with your favorite movie viewer. All these movies require the Techsmith Screen Capture Codec in order to play properly. We recommend the Camtasia Player (also from Techsmith) as a viewer for our movies.