GeoGebra Discovery
いわゆる対話型幾何学ソフト（https://en.wikipedia.org/wiki/List_of_interactive_geometry_software）における"証明"のサポートは，形式的証明の作成支援とシンボリックな座標計算への翻訳とに大別できます．今回の GeoGebra Discovery はこの後者であり，Giac による Groebner 基底などの計算と realgeom が呼び出す Mathematica や QEPCADB/tarski などによる QE を統合して「ユーザーが指定した 1 つの点，或いは，合同変換不変量（長さや面積）についての 2 つの有理式」に関した定理を自動生成するものです．
・geogebra-discovery
https://github.com/kovzol/geogebra-discovery
https://youtu.be/useer6QEelA
https://youtu.be/N_Ls5YC-Vaw
"Connecting Mathematica and GeoGebra to explore inequalities on planar geometric constructions" (2019)
https://www.researchgate.net/publication/337499551
"GeoGebra and the realgeom Reasoning Tool" (2020)
http://ceur-ws.org/Vol-2752/paper15.pdf
benchmarks
https://prover-test.geogebra.org/job/GeoGebra_Discovery-comparetest/lastSuccessfulBuild/artifact/fork/geogebra/test/scripts/benchmark/compare/html/all.html
https://prover-test.geogebra.org/job/GeoGebra_Discovery-comparetest/46/artifact/fork/geogebra/test/scripts/benchmark/compare/html/public.html
"Geometric Inequalities" (1968)
https://www.isinj.com/mt-usamo/Geometric%20Inequalities%20-%20Bottema,%20et.%20al.%20(1968).pdf
・realgeom
https://github.com/kovzol/realgeom
https://github.com/kovzol/realgeom/blob/master/src/test/resources/benchmark.csv
http://htmlpreview.github.io/?https://github.com/kovzol/realgeom/blob/master/demo/benchmark.html
・Giac
https://www-fourier.ujf-grenoble.fr/~parisse/giac.html
"Giac and GeoGebra – Improved Gröbner Basis Computations" (2015)
https://www.researchgate.net/publication/277475144
・使用例
上の構成で Input : Compare(a+b, c) により生成される Mathematica のコマンドは次の通りです．
code=ToRadicals[Reduce[Resolve[Exists[{v5,v6,v9,v10,v8,w1},(m>0) \[And] (v8>0) \[And] (v9>0) \[And] (v5^2-2*v5+v6^2-v9^2+1==0) \[And] (v10*v6-1==0) \[And] (v5^2+v6^2-v8^2==0) \[And] (v8+v9-w1==0) \[And] (-m+w1==0)],Reals],Reals],Cubics->False]コマンドの内容は，座標，長さなどを束縛変数，ユーザーが指定したそれらについての 2 つの有理式の比の値を自由変数とする等式や不等式の連言の存在量化を QE するもので，ユーザーへの出力表示は単なる相等，大小関係ながら，実際には比の値域を特定しており，前処理として Giac が不要な変数を消去，適当な 2 点を (0, 0)，(1, 0) とするなどの工夫が施されていますが，図形が退化しないための変数の非零条件は新たな束縛変数との積が 1 と翻訳されること，及び，正多角形の頂点の座標の特定に不等式制約を付さない為，下記の例や上掲の 2 つめの動画の 4:30 からのように不要な式との選言が出力される場合があることには注意を要します．また，CAS のタイムアウト（GeoGebra-Discovery ファイルにて指定）は 10 秒なので，Mathematica の別セッションに code をコピペ実行するのが現実的かも知れません．
なお，Mathematica（realgeom 自体は Maple，REDUCE にも対応）がインストールされていない環境でも，本ツールに（WIndows版を含め）同梱されている QEPCADB/tarski が機能します．下記は正 5 角形の辺，対角線の長さの比 m の値域を得る際に生成されるもので，tarski に呼び出された QEPCADB が QE した結果を Giac が改めて簡約しています．
2021-05-14 20:53:27.13 LOG: code=(def process (lambda (F) (def L (getargs F)) (def V (get L 0 0 1)) (def B (bbwb (get L 1))) (if (equal? (get B 0) 'UNSAT) [false] ((lambda () (def G (qfr (t-ex V (get B 1)))) (if (equal? (t-type G) 6) (qepcad-qe G) (if (equal? (t-type G) 5) (qepcad-qe (bin-reduce t-or (map (lambda (H) (qepcad-qe (exclose H '(m)))) (getargs G)))) (qepcad-qe G)))))))) (process [ ex v10,v7,v6,v12,v9,v11,v14 [v14>0 /\ v10 v7-2 v7 v6-v12+v6 v9+v6=0 /\ -v10 v6+v6^2-v11-v7^2+v7 v9+v7=0 /\ v6^2+v7^2-2 v7=0 /\ 4 v7^2-6 v7+1=0 /\ -v10+2 v6 v7-v6=0 /\ -v6^2+v7^2-v7-v9+1=0 /\ v10^2-v14^2+v9^2=0 /\ -m+v14=0]]) [m^2 - m - 1 <= 0 /\ m^2 + m - 1 >= 0 /\ [m^2 - m - 1 = 0 \/ m^2 + m - 1 = 0]]:tar 2021-05-14 20:53:27.581 LOG: result=m^2 - m - 1 <= 0 /\ m^2 + m - 1 >= 0 /\ [m^2 - m - 1 = 0 \/ m^2 + m - 1 = 0] 2021-05-14 20:53:27.581 LOG: mathcode=solve([(m^2 - m - 1 <= 0),(m^2 + m - 1 >= 0),(m^2 - m - 1)*(m^2 + m - 1),(m>0)],m) 2021-05-14 20:53:27.589 1/2*(sqrt5-1),1/2*(sqrt5+1)
