用OK Geometry生成的几何问题

hbghlyj

设 ABC 为锐角三角形。
点 D 和 E 位于边 BC 上，且 D 位于 B 和 E 之间，AD = CD，AE = BE。
点 F 是满足 FD∥AB 和 FE∥AC 的点。
证明 FB = FC。

根据Automated Generation of Planar Geometry Olympiad第 58 页，作者在他的软件 OK Geometry 上的大规模实验中生成了问题（第 3.2 节）。整个运行时间总共约为 40,000 CPU 小时，最长运行时间约为 40 小时。这五道题目被提交给 2020 年国际数学奥林匹克竞赛，第一道题被 IMO 采用，即上面的题。

hbghlyj

有关该软件如何帮助生成 IMO 2020 问题 4 的故事，请参阅 AoPS 论坛帖子

artofproblemsolving.com/community/c6h2883216p25677071
I started with a cyclic quadrilateral $SCDQ$ (this is a step of the solution to the original problem) with $T$ being the intersection point of its diagonals.

I wanted some equal lengths to create magic - so I thought I would draw points $B$ and $E$ on the internal bisector of $\angle STC$ such that $TB=TD$ and $TE=TC$ and $B,T,E$ lying on a line in this order.

I put this into my software GeoGen and it suggested two things:

1. If I intersect $BQ$ and $SE$ at $A$, I'd have $AB=AE$.
2. If I intersect both $AB$ and $SE$ with $CD$ at $P$ and $R$, I'd have $P,Q,R,S$ concyclic.

I proved these two, understood the situation and then restated it.

In my first version, I had $B,T,E$ collinear and $AB=AE$. One day before the deadline for proposals, I was reviewing my solution and realized I'm not using the collinearity of $B,T,E$ that much - it dawned on me I can just have $\angle ABT = \angle AET$ and the proof would still work. And that was the end.

I'm very happy about the problem being used. Not so happy that it was the only geometry, just like many of us.

hbghlyj

在AoPS搜索geogen关键词，已有许多帖子将“问题来源”标注为geogen
甚至有一篇帖子的标题为Computer too strong

相关：AlphaGeometry