Table of Contents
Fetching ...

Solving Some Geometry Problems of the Náboj 2023 Contest with Automated Deduction in GeoGebra Discovery

Amela Hota, Zoltán Kovács, Alexander Vujic

TL;DR

This paper tackles solving geometry contest problems with automated deduction in GeoGebra Discovery, leveraging symbolic computations to produce verifiable results rather than numerical approximations. It adopts the Recio-Vélez elimination framework to extract length ratios, demonstrated on Náboj 2023 problems, with Problem 6 yielding a symbolic relation $P = 8\\sqrt{2}\\cdot s$. The key contributions include concrete solvable cases (Pentominos, Right Triangle, Triangle and Circle) and a candid discussion of current limitations in angle and area handling, plus implications for contest design and educational use. The work highlights the practical potential of symbolic geometry tools for rapid, exact reasoning in competition settings and suggests future extensions to support broader classes of geometric quantities and implicit reasoning.

Abstract

In this article, we solve some of the geometry problems of the Náboj 2023 competition with the help of a computer, using examples that the software tool GeoGebra Discovery can calculate. In each case, the calculation requires symbolic computations. We analyze the difficulty of feeding the problem into the machine and set further goals to make the problems of this type of contests even more tractable in the future.

Solving Some Geometry Problems of the Náboj 2023 Contest with Automated Deduction in GeoGebra Discovery

TL;DR

This paper tackles solving geometry contest problems with automated deduction in GeoGebra Discovery, leveraging symbolic computations to produce verifiable results rather than numerical approximations. It adopts the Recio-Vélez elimination framework to extract length ratios, demonstrated on Náboj 2023 problems, with Problem 6 yielding a symbolic relation . The key contributions include concrete solvable cases (Pentominos, Right Triangle, Triangle and Circle) and a candid discussion of current limitations in angle and area handling, plus implications for contest design and educational use. The work highlights the practical potential of symbolic geometry tools for rapid, exact reasoning in competition settings and suggests future extensions to support broader classes of geometric quantities and implicit reasoning.

Abstract

In this article, we solve some of the geometry problems of the Náboj 2023 competition with the help of a computer, using examples that the software tool GeoGebra Discovery can calculate. In each case, the calculation requires symbolic computations. We analyze the difficulty of feeding the problem into the machine and set further goals to make the problems of this type of contests even more tractable in the future.
Paper Structure (11 sections, 3 equations, 18 figures)

This paper contains 11 sections, 3 equations, 18 figures.

Figures (18)

  • Figure 1: Problem setting 6 and the official solution of Náboj 2023
  • Figure 2: Sketching Problem 6 in GeoGebra Discovery
  • Figure 3: Report of a symbolic analysis of Problem 6 in GeoGebra Discovery
  • Figure 4: Problem setting 15
  • Figure 5: Problem setting 15 in GeoGebra Discovery
  • ...and 13 more figures