Phil Scott, Jacques D. Fleuriot: An Investigation of Hilbert's Implicit Reasoning through Proof Discovery in Idle-Time. Automated Deduction in Geometry 2010: 182-200