A Theorem Prover that Computes?

Why do we want to prove a theorem? Because we are lazy. We do not want to test infinite many cases, we want verification for all cases at once. The objective of Bruno Buchberger's Theorema project is to let the computer construct the proof. An automatically generated proof of the shown theorem, see here . The proof is white-box (readable) and it uses an external operation (Simplify) provided by Mathematica. Theorema is built on top of Mathematica. We could have done this proof easily by hand, but if we look at the Nontrivial Example... ? The long-term objective of the Theorema project is to produce a complete system which supports the mathematician in creating interactive text books. This covers the mathematical problem solving cycle including specification, exploration, creating ideas, proving and programming.
Programming? Simplified, the constructive proof that the Groebner Bases are result of correct equivalence transformations (of the original system of polynomials) is a program which computes them. The automatically generated proof is computational.
To my knowledge, Mathematica was selected for Theorema because it allows to define your own syntax, its pattern matching mechanism and comprehensive solvers.


  1. As they value relatively highly the views of their peers (Adhami, Johnson et al. 1995) social interaction dominated by the teacher is likely to result in limited learning gains compared to carefully constructed learning opportunities where pupils feel autonomous and independent and teachers act as guides. how to master math

    1. Totally agree, explorative, constructive learning arrangements ...

      Even more general: lectures "kill" innovation.