It's a question that's been bothering me for a long time,pls!!!

[Ceiso1]

It is known that △ABC is an equilateral triangle, and points E, D, and F are three points inside the triangle, connecting AD, BE, and CF, and points E, F, and D are exactly on AD, BE, and CF respectively, and satisfy AE = CD = BF. Prove that △EFD is an equilateral triangle.

This question is very difficult for me many nights, I can not help but deploy AlphaGeometry in order to solve this question, after the deployment is completed because of the language of AlphaGeometry, and difficult to me for a long time, I see that the big brother of the AlphaGeometry to improve, so I hope to get some guidance!!!

Please!!!

[Ceiso1]

I would like to know how to prove this question and how this question should be translated into AlphaGeometry's language, hopefully you can see my issue

[tpgh24]

I don't think this problem can be expressed in AlphaGeometry's problem definition language. This language requires one to construct points one by one, similar to how one draws a figure using compass and straight edge. Problems that cannot be constructed this way but must rely on a constraint cannot be expressed by this language. In this problem, I don't think you can get around a constraint. For example, if you first draw the triangle ABC then point D, from AE=CD you can find E, then from the intersection of BE and CD you can find F, but then you have to rely on a constraint AE=BF to narrow down the position of D. This is a limitation that the authors of AlphaGeometry acknowledged.

The problem can be proved by contradiction. First prove that $\angle BAE = \angle CBF = \angle ACD$. If this is not true, without loss of generality, assume $\angle BAE$ is the biggest among the three angles, then $BE>CF => EF>FD => \angle EDF > \angle FED => \angle CAD + \angle ACD > \angle ABE + \angle BAE$. Since $\angle BAE > \angle ACD$, we must have $\angle CAD > \angle ABE$. Combined with $\angle BAE > \angle CBF$, this implies $\angle CAB > \angle ABC$, but this contradicts with the premise that $ABC$ is an equilateral triangle. From $\angle BAE = \angle CBF = \angle ACD$ it's easy to prove that $DEF$ is equilateral.

By the way, this kind of proof that utilizes inequalities are also out of the scope of AlphaGeometry.

[Ceiso1]

First of all, thank you for your answer, but this question I know can be proved by contradiction also known as the inverse method, in fact, this question I have asked a lot of people, without exception, said that there is no other way except the inverse method, we all think for a long time for this question, rotate the vector coordinates, etc., there is no way to do so, so I would like to try to use the AlphaGeometry for the proof of the question, I make the question I described the problem in the language of AlphaGeometry, but I couldn't proceed because of the problem of the construction point. Since it's a limitation of AlphaGeometry, it seems that the problem can't be proceeded any further, thank you for your answer!

[tpgh24]

I tried algebraic methods and there doesn't seem to be a "direct" method either. Let $\angle DAC=a, \angle EBA=b, \angle FCB = c, \frac{AE}{AB} = \frac{BF}{BC} = \frac{CD}{CA} = k$, by law of sine, $\sin(a) = k \sin(a+60-c)$ and so on for two more such equations. There doesn't seem to be a direct way to solve these equations to conclude $a=b=c$. You can convert the trigonometry equations to polynomial ones but they are not much better. The only solution I can find also depends on an argument similar to inequality. If we view $c$ as a function of $a$ implicitly defined by the equation above $c=f(a)$, similarly we have $b=f(c), a=f(b)$ so $a=f(f(f(a)))$. Using derivatives, it's easy to see $f(a)$ is monotonically decreasing when $a, b, c < 60, 0 < k < 1$, so function $f(f(f(a)))$ is also monotonically decreasing, so $a=f(f(f(a)))$ only has one solution and that's when $f(a)=a$.