Profile cover photo
Profile photo
Cris Perdue
“No man ever steps in the same river twice, for it's not the same river and he's not the same man.” ― Heraclitus
“No man ever steps in the same river twice, for it's not the same river and he's not the same man.” ― Heraclitus

Cris's posts

Post has attachment
Extended abstract titled "Creating Usable Computer Tools that Reason Mathematically", presented at the ThEdu'15 workshop, part of CICM 2015. This gives an overview of motivations and approaches taken in Mathtoys to make a usable interactive assistant for working on textbook algebra problems.

Post has attachment
Slides of my talk at the ThEdu'15 workshop on Theorem-proving components in education last week, part of CICM 2015.

Project home officially moved to GitHub.

Mathtoys and the Prooftoys engine that powers it are now officially moved to GitHub. The project was originally hosted on Google Code, but Google Code is shutting down, and source code management has moved from Mercurial to Git. Fortunately it was not necessary to lose any revision history, and GitHub has many great tools for anyone involved in development of a project.

Repositories on Google Code and will not receive updates to the source code in the future., and will eventually be removed.

Post has attachment
Happy Pi Day!

In honor of this day here is a link to an article about the wonder of mathematics in science, and physics in particular. The article is "The Unreasonable Effectiveness of Mathematics in the Natural Sciences" ( by Nobel Prize winner Eugene Wigner.

You may not want to read the entire article, so let me quote the conclusion:

"The miracle of the appropriateness of the language of mathematics for the formulation of the laws of physics is a wonderful gift which we neither understand nor deserve. We should be grateful for it and hope that it will remain valid in future research and that it will extend, for better or for worse, to our pleasure, even though perhaps also to our bafflement, to wide branches of learning."

Changes in the Mathtoys Engine

Up to now the Mathtoys proof engine has been based on mathematical foundations like the ones used by the HOL family of interactive “proof assistants”. These foundations have made it easy to build the kinds of proofs Mathtoys needs to do. In Mathtoys though it is also very important to use notation that is as standard as possible, and this is motivating some changes to some of the concepts in the Mathtoys proof engine. These changes will also mean that users of Mathtoys who are interested in some kinds of advanced mathematics will find that the Mathtoys concepts match the ones they will expect.

Proofs seen in Mathtoys will still be very much the same as they have been in the past. Some internal proofs “under the hood” will change though and some new proofs will be different than they would be with the original proof engine.

These changes are not yet implemented. I will keep you up to date as they become available in Mathtoys.

New posting on the Mathtoys blog - "The math problem inside every math problem" ( 

Post has attachment
The math problem inside every math problem
A great deal of high school math is about
solving problems. Yet for mathematicians throughout history and right
up to the present, math is about proofs. Are students doing one kind
of math, while mathematicians are doing something quite different?
Not reall...

Please note that the posting "Vacuously true statements" has moved to the new Mathtoys blog at

Post has attachment
This posting has moved from Google Drive to the new

Post has attachment
The meaning of “implies”
Nothing is more essential to mathematical thinking than deduction, the art of working out the consequences of precise assumptions, in other words their implications. We are going to take a closer look at the mathematical meaning of “implies” through an exam...
Wait while more posts are being loaded