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

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.

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."

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

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

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.

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

What is Mathtoys?

Mathtoys is a project to produce a computer tool that ordinary people with an interest in math can enjoy using to understand and solve mathematical problems.

Post has attachment
Wait while more posts are being loaded