Questions and answers

Q: I still have a question on my mind. What can I do about that?

A: Please don’t be shy to start a GitHub discussion or contact the author.

Q: What makes you think it is worthwhile to be so formal about reasoning?

A: This question is worth a longer answer, but here is my point of view in brief.

• Mathematical reasoning is a skill that carries over beyond standard techniques. It is essential to reading explanations produced by a computer. Along with mathematical intuition, it gives you the potential to solve different kinds of problems and create new mathematical knowledge. These things will be relevant as long as human beings are involved in mathematics.
• Proper computer reasoning is necessarily precise and formal. It comes with some big benefits such as smart tools that give reliable results.

Q: Can principles of basic algebra really handle advanced mathematics?

A: The power of simple principles to solve complex problems is part of the wonder of mathematics. In fact Prooftoys does employ just a couple of simple extensions to basic algebra, but mostly it applies the same principles from algebra in more general ways.

Q: Do you seriously think I can “pick up” Prooftoys without a lot of studying?

A: Yes, seriously! Try a few of the simplest sample problems and see how it feels. You may find that getting simple things done is not hard at all. You can use the proof builder without understanding a lot about logic. If it fails in this, please contact the author. I would love to hear from you.

Properly grasping the meaning of mathematical statements may take a bit longer. You can start by ignoring the parts that aren’t shown in a typical textbook. As you understand the language of mathematics better you can pay more attention to them.

Q: But is it useful for “textbook” math problems?

A: In fact it can help you solve problems quickly and accurately, but you will need to invest some time in learning to use it and getting familiar with explicit mathematical reasoning.

Q: Can it help me with my math homework?

A: If you are just trying to get today’s homework done today, Prooftoys is probably not worth the effort. If you would like help getting through your homework for the rest of the year, then perhaps yes. Once you get familiar with the basics, the same concepts carry over directly to other topics. And if you want to strengthen your mathematical skills and your grasp of mathematical concepts, then Prooftoys should be able to really shine for you.

Q: Please don’t tell me you want to change the mathematics curriculum.

A: No, I believe that changes to the curriculum can only occur in the event of overwhelming demand for change, and then only with much pain. This project only aims to give some people the chance to try a fresh approach and hopefully to help point a way forward.

Q: Why should I spend time here when there are Khan Academy, Geogebra, Wolfram Alpha, and many other mathematics websites?

A: Prooftoys is about mathematical reasoning. The user interface keeps you always in control while assuring that your reasoning is mathematically correct. You solve the problem or prove the theorem yourself, while the engine correctly takes care of the details. As you work, presentation of the reasoning is in textbook-like form.

None of these “math help” website offers this, and to my knowledge no other math help website is backed by a computer implementation of mathematical logic.

Q: Is Prooftoys or its logic really that unique?

A: Well, yes and no. Very close relatives of the simple type theory used here are implemented in “research-grade” proof assistant software, but hardly any textbooks present this kind of logic.

First-order logic is presented in many textbooks. Simple type theory has important practical and technical advantages, and Prooftoys combines them with a modern point-and-click user interface.

Q: My interest is learning about mathematical proof using a textbook such as “The Book of Proof” or similar resource. Why shouldn’t I learn about proof from my well thought-out book?

A: You may be very happy with your book. In fact, support for reasoning in the style of books of this kind is an important goal for Prooftoys and the proof builder.

If you are teaching yourself, you may find that Prooftoys helps to “keep you honest”, not skipping steps or waving your hands. The downside can be that computers and computer implementations of logic are very precise and explicit, so Prooftoys may feel nit-picky at times.

Q: Tell me more about this type theory.

A: See the technical notes for more information about type theory and Prooftoys’ use of it.

Q: Where is the set theory?

A: Like many modern proof assistants, Prooftoys is based on simple type theory rather than set theory. Type theory enables us to get on very directly to talk about things like numbers without theorizing about sets first.

Q: Is there something weird about this logic? When I look at theorems with quantifiers for example, I see things like forall P. What’s up with that?

A: No, the principles behind Prooftoys are about as standard as can be. The notation is sometimes a bit different though. Anywhere you see something like forall P you can read it exactly as forall x. P x in a more traditional notation.