How Does It Work Inside?

MathCheck works by trying many (combinations of) values of variables

• reports an error, if it finds a counter-example
• may fail to find a counter-example

MathCheck uses

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

Sometimes also a positive answer is certain: = ≥ ⇔

• in some cases, it is possible to test with all values
• MathCheck does contain a tiny proof engine