@article{Kovács2023, 
author = {Zoltán Kovács and Tomás Recio and Carlos Ueno and Róbert Vajda},
title = {The "never-proved" triangle inequality: A GeoGebra & CAS approach},
year = {2023},
journal = {AIMS Mathematics},
volume = {8},
number = {10},
pages = {22593-22642},
keywords = {triangle inequality, elementary geometry, automated reasoning, dynamic geometry, computer algebra systems, inscribed triangle},
url = {https://www.sciopen.com/article/10.3934/math.20231151},
doi = {10.3934/math.20231151},
abstract = {We use a quite simple, yet challenging, elementary geometry statement, the so-called  "never proved" (by a mathematician) theorem, introduced by Prof.  Jiawei Hong in his communication to the IEEE 1986 Symposium on Foundations of Computer Science, to exemplify and analyze the current situation of achievements, ongoing improvements and limitations of GeoGebra's automated reasoning tools, as well as other computer algebra systems, in dealing with geometric inequalities. We present a large collection of facts describing the curious (and confusing)  history behind the statement and its connection to automated deduction.   An easy proof of the "never proved" theorem, relying on some previous (but not trivial) human work is included. Moreover, as part of our strategy to address this challenging result with automated tools, we formulate a large list of variants of the "never proved" statement (generalizations, special cases, etc.).  Addressing such variants with GeoGebra Discovery,              Maple      ,              REDUCE/Redlog       or              Mathematica       leads us to introduce and reflect on some new approaches (e.g., partial elimination of quantifiers, consideration of symmetries, relevance of discovery vs. proving, etc.) that  could be relevant to consider for  future improvements of automated reasoning in geometry algorithms. As a byproduct, we obtain an original result (to our knowledge) concerning the family of triangles inscribable in a given triangle.}
}