30 July 2024

Automated measuring the difficulty of geometric theorems

This entry summarizes some achieved results and the planned future work on automated measuring the difficulty of geometric theorems.

Some references for the newcomers: It is wonderful news that our software presentation won the Distinguished Software Demonstration Award this year at ISSAC.

Here are some on-going work and further ideas as next steps to continue this project:
  1. Soma Bartha and András Kerekes were involved in testing GeoGebra Discovery's ShowProof command in the frame of a GeoGebra internship this summer. We have a database of more than 25 geometry statements from high school lecture notes, collected by their mathematics teachers János Schultz and János Mike, during several years of teaching experience at Radnóti Miklós Secondary School in Szeged, Hungary. The test cases are named with SB-*.ggb in the test folders true and false of GeoGebra's fork. An on-going work is to analyze these tests and give a detailed report for a Hungarian journal in mathematics education.
  2. András implemented the GeoGebra files from the above mentioned database in Java Geometry Expert (JGEX). His analysis on the results will be added to the Hungarian report.
  3. We are hoping that there is some correlation between the algebraic difficulty and the geometric complexity of these statements. A manual comparison by computing statistical correlation between the outputs of GeoGebra Discovery's algebraic difficulty degree and the outputs of JGEX (the number of used derivation steps in the GDD method) could be an interesting further step. András already collected not just the derivation steps but the height of the GDD derivation tree (among other information). Computing the correlation for the above database is another step for the project.
  4. Since we have a larger database of more than 300 statements, it would be interesting to obtain the above statistics automatically, without the requirement to construct each GeoGebra file manually in Java Geometry Expert. Therefore, a full version of the GGB importer in JGEX would be a mandatory step. This requires some Java programming in DrawProcess.java, by implementing all missing GeoGebra commands. This subproject will require several days of work, but it should be more or less straightforward if someone starts it with some intermediate Java programming skills. Please let me know if you are interested in this.
  5. A different kind of programming task is to extend the ShowProof command to accept a second parameter. It is usually a good idea to have an updated construction with equations and labels that contain the corresponding formulas. But sometimes the user does not want that. In such cases, it would be useful to avoid updating the construction and leave it as is. This subproject has already been started by Jonathan Yu.
  6. Jonathan also did some preliminary programming to have full cover off all the 300+ statements by exact descriptions for each variables that require auxiliary definitions. These are called variable Botana variable descriptions. After having a list of the missing descriptions, someone should finalize this part of the program. Also, a double-check of all automatically created ShowProof outputs would be beneficial for the project.
  7. There are promising improvements in the output of GDD's GraphViz output. This is on-going work with András and Alexander Vujic, a master student at PHDL, Linz, Austria.


    A possible export of the GDD proof tree for JGEX's example 15

  8. Yet another project for a Hungarian journal: To give a full analysis on the Pete-Dőtsch theorem, by using the ShowProof command. It is unclear if this should be a part of the work with Soma and András, or maybe I will write that paper as extra work.

Continue reading…

See also a filtered list of the entries on topics GeoGebra, technical developments or internal references in the Bible.

Zoltán Kovács
Linz School of Education
Johannes Kepler University
Altenberger Strasse 69
A-4040 Linz