How Does MathCheck Work?

Most modes work by trying many (combinations of) values of variables

• reports an error, if it finds a counter-example
• may fail to find a counter-example
• room for improvement: better detection of division by 0

In equation mode

• teacher-given roots are always checked
• explicit student-given roots are checked while not in the scope of ⇒
• room for improvement: detect superfluous roots earlier

MathCheck uses

• precise rational number arithmetic when it can
• floating point interval arithmetic other times
• it is actually more complicated
• rounding errors do not cause false alarms, but some true alarms may be lost
• 10^308 = 10^309

Sometimes also a positive answer is certain: = ≥ ⇔

• in some cases, it is possible to test with all values
  ⇒ the modular arithmetic mode
• MathCheck contains a tiny proof engine
  sin^2 om = 1 - cos^2 om >= 0

A 10-second course in recursive function theory:

Nobody can write a computer program that answers
every mathematics question correctly in finite time

⇒ Every MathCheck-like program is imperfect in one way or another

• e.g., Wolfram Alpha deems (-8)^(2/3) = 4 as false by default
• please be realistic in your expectations!