The scientific man does not aim at an immediate result. He does not expect that his advanced ideas will be readily taken up. His work is like that of the planter – for the future. His duty is to lay the foundation for those who are to come, and point the way. — Nikola Tesla
About Prooftoys.org
Welcome! The Prooftoys website and its software are ongoing experiments in creating computer aids to help human beings learn and do mathematics. The application software is proudly open source, hosted at Github, primarily in the crisperdue/prooftoys repository.
The key goal is to create a computer math tool or tools that are easy, highly available, useful, attractive, and valuable to people learning (or doing) mathematics, especially newcomers, for reading and writing proofs, and for solving problems deductively.
The larger vision is to develop the kind of user experience that can bridge the gap between computer proof technology and ordinary people learning to understand and use mathematics.
About the logic
The logic of Prooftoys is a form of simple type theory, based rather directly on the theory Q0 of Carnegie Mellon University Professor Peter B. Andrews. See the tech notes for more details.
Getting in touch
One goal is to develop a friendly community of users around the tools here and their goals of using computers for mathematical reasoning. Don’t hesitate to say “hello” to the author through email.
Sincerely,
Cris Perdue