Mechanised reasoners can be used both to check existing proofs as well as to conjecture and prove new results.  They have, for example, discovered a proof of Robbins’ conjecture, and confirmed a proof of Kepler’s conjecture that had exhausted a committee of twelve referees.  Applied to economic problems, they have helped find a generalisation of Arrow’s theorem, and automatically produced 84 impossibility theorems in the ‘ranking sets of objects’ problem. We introduce mechanised reasoning, its use to date within economics, illustrating particularly via auction theory (Vickrey’s theorem) and practice (a soundly specified and implemented combinatorial auction).