27 October 2021
Embedding Tarski in GeoGebra delivers
discovery of geometric inequalities on the web
After a couple of weeks of work I am happy to announce that GeoGebra is now
able to discover geometric inequalities in its web version. In this blog entry you can try it on your own.
Please follow these steps:
Click on the 5. toolset in the Toolbar and select the first tool (Polygon
- Draw a triangle in the Graphics area (on the right) by creating three points, and then click on the first point again.
Click on the last, empty line in the Algebra view (on the left) and type Relation(a+b,c) and press ENTER.
GeoGebra will inform you that \(a+b\) and \(c\) differ. But by clicking on the More... button
some further computation will start. In a couple of seconds you will obtain the triangle inequality.
Finally you can safely close the popup window by clicking OK.
The computations are performed here by the web version of Tarski
a program that is able to symbolically solve
systems of inequalities, and allowing quantifiers as well.
Compilation of Tarski for the web was not completely straightforward. The first steps were described
in my blog
. Additionally, Tarski had to be compiled as a JS module by using
the linker flags SINGLE_FILE
and a unique EXPORT_NAME
had to be given.
The first flag helped in embedding the .wasm object in the .js file to simplify inclusion of the WebAssembly code
in a webpage. The second and third flags allowed that Tarski did not conflict with another WebAssembly module:
in GeoGebra we already use Giac in the same way.
Loading Tarski for the web can be performed with the following JS code:
var numcells = 50000000;
var timeout = 5;
TARSKIINIT = Module.cwrap("TARSKIINIT", 'void', ['number', 'number']);
TARSKIEVAL = Module.cwrap("TARSKIEVAL", "string", ["string"]);
TARSKIEND = Module.cwrap("TARSKIEND", "void", );
Using an embedded version of Tarski is beneficial also for the desktop version. It does not require the
application any longer. Now the
important parts of realgeom are embedded
in GeoGebra Discovery.
This accelerates the startup of GeoGebra Discovery a lot! If you are interested, you can give
the new desktop version a try by downloading it
Embedding Tarski into the desktop version was more or less smooth. Here the only challenge was
to carefully communicate with SWIG
that Tarski will be a
and not a standalone application.
The examples provided above are all managable and stable. Of course, there are many examples that
are more challenging or even infeasible to compute. Here I focus on another example, namely
Bottema's theorem 5.3 (published in the book Geometric Inequalities, 1968,
co-authored with Djordjevic, Janic, Mitrinovic and Vasic). It is about comparing the
perimeter \(a+b+c\) and the circumradius \(R\) of an arbitrary triangle. One can show that
\[a+b+c\le3\sqrt3\cdot R\] for all triangles.
It turns out that different geometric realizations may lead to different computations
with different difficulties. To define the radius one needs to create the circumcenter first,
and then one of the three vertices must be chosen to designate the circumradius, but this choice
is actually free: it depends on the user. But the computational complexity depends a lot on
the user's decision!
For example, we can learn that connecting the circumcenter
with point A is the preferred method, and choosing the perpendicular bisectors for sides b
and c results in the fastest computation. Other choices (like A plus a and b
or b plus a and b) will, in our tests, usually result in twice slower
computations, or, what is even worse (like selecting C or a and b),
the computation may take lots of minutes or even hours...
What does this mean in numbers? We focus on the fastest method, that is, we choose to designate R by connecting
A and the circumcenter which will be defined as the intersection of perpendicular bisectors
for sides b and c. We compared the timings on four platforms.
First, a Linux system was tried with a CPU Intel(R) Core(TM) i7-8550U CPU @ 1.80GHz. Here the timing was 631
milliseconds on the desktop version of GeoGebra Discovery, not bad.
The same test in Google Chrome 95.0.4638.54 gave 6886 ms, almost ten times slower
than in the desktop version. In Firefox 93.0 the timing was 21842 ms: another three times slower. This is
clearly not acceptable any longer in a classroom situation.
For the web platforms we started some further experiments. Web browser improvements promise the
nearby implementation of C++ exceptions
By using the experimental feature wasm-exceptions
(and recompiling Tarski accordingly) we can speed up
the computation to get 4266 ms in Google Chrome 95 and to get 15924 ms in Firefox Nightly 95.0a1 (2021-10-24).
So we can spare quite a lot of time! But still, there is some bottleneck somewhere, because the
web version is still much behind the desktop version in performance.
See also a filtered list of the entries on topics GeoGebra
, technical developments
or internal references in the Bible