关于IBM的等边三角形问题

zeus

原题：
翻译：三角形ABC，点D在AB上，E在BC上，F在CA上，小三角形DEF是等边三角形，AD=BE=CF，证明ABC是等边三角形。
这个表述中，点在边上的表述是有点问题的，如果允许点在边所在的直线上，那么可以构造这样一个三角形：

{PA -> Root[
   776400390064828305390058242299723776 -
     6750468112004492168995421349812109312 #1 +
     28256463057734058842680079946066274816 #1^2 -
     75293808396454886252627944631235640320 #1^3 +
     142275546782627452440260927355468859545 #1^4 -
     200757338119961071755171026906990190792 #1^5 +
     216462517319981146208078022970613928224 #1^6 -
     178824190278442443091041073481975728692 #1^7 +
     111260078290860063059896472006840124320 #1^8 -
     49876762319637082998717457494378250920 #1^9 +
     14591664029304933540358057849519126166 #1^10 -
     2083623387254226098536848771021817512 #1^11 -
     68156646539443335317920522966768224 #1^12 +
     10183945134850496161340190526269900 #1^13 +
     27221439670203422794141768733658400 #1^14 -
     5912640887663565584787490828365000 #1^15 +
     439405363613503804852856740905625 #1^16 &, 16], PB -> 0, PC -> 1,
PD -> Root[
   30694686286270049289708010000 + 68425426089864953788237020000 #1 -
     37910739947917548878059818600 #1^2 -
     1126924248019425586748531929800 #1^3 +
     7222989856172705510479834409249 #1^4 -
     18611457618292774165181396714184 #1^5 +
     99636403785905157197432269537688 #1^6 -
     286257913727056480881923710395552 #1^7 +
     515295796056449104965553437284880 #1^8 -
     711197796182556019497078880862208 #1^9 +
     856678549526682242959033939755008 #1^10 -
     668776294688719472632126846795776 #1^11 +
     228558240043725918618864523935744 #1^12 +
     43972134431780610425389213286400 #1^13 -
     14955636288293237178049862041600 #1^14 -
     11465042059260535750514442240000 #1^15 +
     5412996496384152276891074560000 #1^16 &, 16],
  PE -> Root[-7889851737109 + 88105952062590 #1 -
     367420585681169 #1^2 + 730057141488892 #1^3 -
     699452335383636 #1^4 + 224328883326976 #1^5 +
     121421565382656 #1^6 - 97244728524800 #1^7 +
     14101564620800 #1^8 &, 4],
PF -> Root[
   1559972561941878645112487483851706503108561 -
     1769497439179132593184168773621668799878698 #1 -
     3000267988684391363232954201502271097841233 #1^2 +
     4261744950413357887287062876964027977870658 #1^3 -
     7351109955469645670244907139895505161720015 #1^4 +
     9542761339898625949056283519194078434726824 #1^5 +
     32483915521840719625104802604853689801880584 #1^6 -
     101948403057409042777431401430881421758424192 #1^7 +
     119674862257013665885168256274531678327879824 #1^8 -
     87527928090926079515132139972470999861493760 #1^9 +
     65713134012279122825482872834446986700095488 #1^10 -
     60859574103744989514143678492109093046583296 #1^11 +
     47492942142659432591489817371643818190831616 #1^12 -
     25280669039581835862778619677040732798976000 #1^13 +
     8307033026568315816940964711605246466457600 #1^14 -
     1366167717938095442276468026198730997760000 #1^15 +
     97897707800091433453686546696597667840000 #1^16 &, 16]}

可验证：AD=BE=CF, 且DE=EF=FD.

mathe

https://bbs.emath.ac.cn/forum.php?mod=viewthread&tid=2383&extra=&highlight=%D5%FD%B6%E0%B1%DF%D0%CE&page=1&mobile=2

mathematica

https://bbs.emath.ac.cn/forum.ph ... 554&fromuid=865
看看九年前的帖子

mathematica

如何证明这个看似结论显然却难以证明的平面几何命题？ - 知乎
https://www.zhihu.com/question/20429750