Buchberger, B.; Jebelean, T.; Kutsia, T.; Maletzky, A.; Windsteiger, W. Theorema 2.0: Computer-Assisted Natural-Style Mathematics. JFR 2016, 9, 149-185.