On automated completion of geometry statements and proofs with GeoGebra Discovery

At the ADG 2023 a protocol, implemented on an extension of Larus automated theorem prover, to automatically complete statements and proofs in Euclidean geometry, was presented by S. T. Gonzalez, P. Janičić, and J. Narboux. The approach is logic-based, in contrast to algebraic methods, and its performance was tested on five high-school level geometry problems. In our contribution we address the same five issues with the automated reasoning, algebraic-based, tools of GeoGebra Discovery. The results allow us to reflect on the pros and cons of these two diverse approaches, showing, in particular, the opportunities that GeoGebra Discovery brings to improve human reasoning in geometry.