A Fully Automatic Theorem Prover with Human-Style Output
Mohan Ganesalingam, W. T. Gowers · Journal of Automated Reasoning · 2016
This paper describes a program that solves elementary mathematical problems, mostly in metric space theory, and presents solutions that are hard to distinguish from solutions that might be written by human mathematicians.