Proof simplification and automated theorem proving

Philosophical Transactions of the Royal Society A, volume 377, issue 2140 (2019),
https://royalsocietypublishing.org/doi/abs/10.1098/rsta.2018.0034