GXWeb is the free browser based version of the symbolic geometry software Geometry Expressions. We demonstrate its use in an educational setting with examples from theorem proving, mathematical modelling and loci and envelopes.
We address, through the automated reasoning tools in GeoGebra Discovery, a problem from a regional phase of the Austrian Mathematics Olympiad 2023. Trying to solve this problem gives rise to four different kind of feedback: the almost instantaneous, automated solution of the proposed problem; the measure of its complexity, according to some recent proposals; the automated discovery of a generalization of the given assertion, showing that the same statement is true over more general polygons than those mentioned in the problem; and the difficulties associated to the analysis of the surprising and involved high number of degenerate cases that appear when using the LocusEquation command in this problem. In our communication we will describe and reflect on these diverse issues, enhancing its exemplar role for showing some of the advantages, problems, and current fields of development of GeoGebra Discovery.
The well known JGEX program became open source a few years ago, but seemingly, further development of the program can only be done without the original authors. In our project, we are looking at whether it is possible to continue such a large project as a newcomer without the involvement of the original authors. Is there a way to internationalize, fix bugs, improve the code base, add new features? In other words, to save a relic found in the attic and polish it into a useful everyday tool.
We examine a class of geometric theorems on cyclic 2n-gons. We prove that if we take n disjoint pairs of sides, each pair separated by an even number of polygon sides, then there is a linear combination of the angles between those sides which is constant. We present a formula for the linear combination, which provides a theorem statement in terms of those angles. We describe a program which uses this result to generate new geometry proof problems and their solutions.
We present simple models of trajectories in space, both in 2D and in 3D. The first examples, which model bicircular moves in the same direction, are classical curves (epicycloids, etc.). Then, we explore bicircular moves in reverse direction and tricircular moves in 2D and 3D, to explore complex visualisations of extraplanetary movements. These moves are studied in a plane setting. Then, adding increasing complexity, we explore them in a non planar setting (which is a closer model of the real situation). The exploration is followed by using these approaches for creating mathematical art in 2D and 3D printed objects, providing new ways of mathematical representations. Students' activities are organized around this exploration.
We give an example of automated geometry reasoning for an imaginary classroom project by using the free software package GeoGebra Discovery. The project is motivated by a publicly available toy, a rocking camel, installed at a medical center in Upper Austria. We explain how the process of a false conjecture, experimenting, modeling, a precise mathematical setup, and then a proof by automated reasoning could help extend mathematical knowledge at secondary school level and above.
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.
In our contribution we describe some on-going improvements concerning the Automated Reasoning Tools developed in GeoGebra Discovery, providing different examples of the performance of these new features. We describe the new ShowProof command, that outputs both the sequence of the different steps performed by GeoGebra Discovery to confirm a certain statement, as well as a number intending to grade the difficulty or interest of the assertion. The proposal of this assessment measure, involving the comparison of the expression of the thesis (or conclusion) as a combination of the hypotheses, will be developed.
We give an insight into Java Geometry Expert (JGEX) in use in a school context, focusing on the Austrian school system. JGEX can offer great support in some classroom situations, especially for solving mathematical competition tasks. Also, we discuss some limitations of the program.
Conjecturing and theorem proving are activities at the center of mathematical practice and are difficult to separate. In this paper, we propose a framework for completing incomplete conjectures and incomplete proofs. The framework can turn a conjecture with missing assumptions and with an under-specified goal into a proper theorem. Also, the proposed framework can help in completing a proof sketch into a human-readable and machine-checkable proof. Our approach is focused on synthetic geometry, and uses coherent logic and constraint solving. The proposed approach is uniform for all three kinds of tasks, flexible and, to our knowledge, unique such approach.
Although there are several systems that successfully generate construction steps for ruler and compass construction problems, none of them provides readable synthetic correctness proofs for generated constructions. In the present work, we demonstrate how our triangle construction solver ArgoTriCS can cooperate with automated theorem provers for first order logic and coherent logic so that it generates construction correctness proofs, that are both human-readable and formal (can be checked by interactive theorem provers such as Coq or Isabelle/HOL). These proofs currently rely on many high-level lemmas and our goal is to have them all formally shown from the basic axioms of geometry.
In 1926-1927, Tarski designed a set of axioms for Euclidean geometry which reached its final form in a manuscript by Schwabhäuser, Szmielew and Tarski in 1983. The differences amount to simplifications obtained by Tarski and Gupta. Gupta presented an independent version of Tarski's system of geometry, thus establishing that his version could not be further simplified without modifying the axioms. To obtain the independence of one of his axioms, namely Pasch's axiom, he proved the independence of one of its consequences: the previously eliminated symmetry of betweenness. However, an independence model for the non-degenerate part of Pasch's axiom was provided by Szczerba for another version of Tarski's system of geometry in which the symmetry of betweenness holds. This independence proof cannot be directly used for Gupta's version as the statements of the parallel postulate differ. In this paper, we present our progress towards obtaining an independent version of a variant of Gupta's system. Compared to Gupta's version, we split Pasch's axiom into this previously eliminated axiom and its non-degenerate part and change the statement of the parallel postulate. We verified the independence properties by mechanizing counter-models using the Coq proof-assistant.
The pursue of what are properties that can be identified to permit an automated reasoning program to generate and find new and interesting theorems is an interesting research goal (pun intended). The automatic discovery of new theorems is a goal in itself, and it has been addressed in specific areas, with different methods. The separation of the "weeds", uninteresting, trivial facts, from the "wheat", new and interesting facts, is much harder, but is also being addressed by different authors using different approaches. In this paper we will focus on geometry. We present and discuss different approaches for the automatic discovery of geometric theorems (and properties), and different metrics to find the interesting theorems among all those that were generated. After this description we will introduce the first result of this article: an undecidability result proving that having an algorithmic procedure that decides for every possible Turing Machine that produces theorems, whether it is able to produce also interesting theorems, is an undecidable problem. Consequently, we will argue that judging whether a theorem prover is able to produce interesting theorems remains a non deterministic task, at best a task to be addressed by program based in an algorithm guided by heuristics criteria. Therefore, as a human, to satisfy this task two things are necessary: an expert survey that sheds light on what a theorem prover/finder of interesting geometric theorems is, and - to enable this analysis - other surveys that clarify metrics and approaches related to the interestingness of geometric theorems. In the conclusion of this article we will introduce the structure of two of these surveys - the second result of this article - and we will discuss some future work.
Proof assistants like Coq are increasingly popular to help mathematicians carry out proofs of the results they conjecture. However, formal proofs remain highly technical and are especially difficult to reuse. In this paper, we present a framework to carry out a posteriori script transformations. These transformations are meant to be applied as an automated post-processing step, once the proof has been completed. As an example, we present a transformation which takes an arbitrary large proof script and produces an equivalent single-line proof script, which can be executed by Coq in one single step. Other applications, such as fully expanding a proof script (for debugging purposes), removing all named hypotheses, etc. could be developed within this framework. We apply our tool to various Coq proof scripts, including some from the GeoCoq library.
In this paper, we present an approach to automated solving of triangle ruler-and-compass construction problems using finite-domain constraint solvers. The constraint model is described in the MiniZinc modeling language, and is based on the automated planning. The main benefit of using general constraint solvers for such purpose, instead of developing dedicated tools, is that we can rely on the efficient search that is already implemented within the solver, enabling us to focus on geometric aspects of the problem. We may also use the solver's built-in optimization capabilities to search for the shortest possible constructions. We evaluate our approach on 74 solvable problems from the Wernick's list, and compare it to the dedicated triangle construction solver ArgoTriCS. The results show that our approach is comparable to dedicated tools, while it requires much less effort to implement. Also, our model often finds shorter constructions, thanks to the optimization capabilities offered by the constraint solvers.
The Naive Angle Method, used by Geometry Expressions for solving problems which involve only angle constraints, represents a geometrical configuration as a sparse linear system. Linear systems with the same underlying matrix structure underpin a number of different geometrical theorems. We use a graph theoretical approach to define a generalization of the matrix structure.
In our contribution we will reflect, through a collection of selected examples, on the potential impact of the GeoGebra Discovery application on different social and educational contexts.
This contribution reports on the continued formalisation of an axiomatic system for Minkowski spacetime (as used in the study of Special Relativity) which is closer in spirit to Hilbert's axiomatic approach to Euclidean geometry than to the vector space approach employed by Minkowski. We present a brief overview of the axioms as well as of a formalisation of theorems relating to linear order. Proofs and excerpts of Isabelle/Isar scripts are discussed, with a focus on the use of symmetry and reasoning"without loss of generality".
Mathematical proof is undoubtedly the cornerstone of mathematics. The emergence, in the last years, of computing and reasoning tools, in particular automated geometry theorem provers, has enriched our experience with mathematics immensely. To avoid disparate efforts,the Open Geometry Prover Community Project aims at the integration of the different efforts for the development of geometry automated theorem provers, under a common"umbrella". In this article the necessary steps to such integration are specified and the current implementation of some of those steps is described.
We report on a new, simple, modular, and flexible approach for automated generation of illustrations for (readable) synthetic geometry proofs. The underlying proofs are generated using the Larus automated prover for coherent logic, and corresponding illustrations are generated in the GCLC language. Animated illustrations are also supported.
