3
$\begingroup$

I am trying to set up Mathematica Synthetic Geometry stuff to prove the following:

Given a triangle ABC with medians $AE$, $BF$, $CD$. Show that we have $\overrightarrow{AE}+\overrightarrow{BF}+\overrightarrow{CD}=0$.

I wrote a piece of code I thought would be useful for this but FindGeometricConjectures won't yield anything useful. How can I create a scene where such conclusion can appear? I know that this can be done much more elementary (without Mathematica's Synthetic Geometry) but I want to learn about Synthetic Geometry.

G = RandomInstance[GeometricScene[
    {a, b, c, d, e, f},
    {
     d == Midpoint[{a, b}],
     e == Midpoint[{b, c}],
     f == Midpoint[{c, a}],
     Triangle[{a, b, c}],
     Line[{a, e}],
     Line[{b, f}],
     Line[{c, d}]
     }
    ]];
FindGeometricConjectures[G]
Improve this question
$\endgroup$

3 Answers 3

Reset to default
4
$\begingroup$

Or prove directly.(This proof also work for 3-dimension or n-dimension)

Clear[n, a, b, c, d, e, f];
n = 2;
d = Mean[{a, b}];
e = Mean[{b, c}];
f = Mean[{c, a}];
Reduce[(d - c) + (e - a) + (f - b) == 
  0, {a, b, c, d, e, f} ∈ Vectors[n]]

True.

Improve this answer
$\endgroup$
4
$\begingroup$

Vectors can be added and subtracted manually by drawing parallel and equal-length line segments.

G = GeometricScene[{a, b, c, d, e, f, o, cd, ae, 
    bf}, {d == Midpoint[{a, b}], e == Midpoint[{b, c}], 
    f == Midpoint[{c, a}], Triangle[{a, b, c}], Line[{a, e}], 
    Line[{b, f}], Line[{c, d}],
    GeometricAssertion[{Line[{o, cd}], Line[{c, d}]}, 
     "MatchingParallel"], 
    EuclideanDistance[o, cd] == EuclideanDistance[c, d],
    GeometricAssertion[{Line[{cd, ae}], Line[{a, e}]}, 
     "MatchingParallel"], 
    EuclideanDistance[cd, ae] == EuclideanDistance[a, e],
    GeometricAssertion[{Line[{ae, bf}], Line[{b, f}]}, 
     "MatchingParallel"], 
    EuclideanDistance[ae, bf] == EuclideanDistance[b, f]
    }];
GeometricSolveValues[G, EuclideanDistance[o, bf]]

(*{0}*)

An Instance

Improve this answer
$\endgroup$
4
  • $\begingroup$ Isn't the OP trying to get M to generate the desired theorem, as opposed to verify it? (As suggested by FindGeometricConjectures in the OP) Alternatively, isn't the OP look for a proof (a sequence of logical reasoning) as opposed to the verficiation of your proof. Those seem more interesting questions to me, and that's how I interpreted the question. (BTW, in V14.1 on my Mac, I get {3.6621*10^-6} instead of (0}.) $\endgroup$
    – Michael E2
    Commented Aug 6 at 15:29
  • $\begingroup$ This is close to what I meant: FindGeometricConjectures[G, HoldPattern[EuclideanDistance[__] == 0]]., though it seems FindGeometricConjectures needs a hint. (OTOH, GeometricSolveValues[G, EuclideanDistance[o, bf] == 0] gives an answer that shows that under the hood, Mathematica uses analytic geometry.) $\endgroup$
    – Michael E2
    Commented Aug 6 at 15:34
  • $\begingroup$ @MichaelE2 Well, OP said he was trying to prove the equation. I tried FindGeometricConjectures[G]["Conclusions"], without any pattern. {EuclideanDistance[o, bf] == 0} is one of the results. I agree that Mathematice uses analytic geometry, but I don't think that would be the reason why you get a result close to 0. If all internal computation use symbols, why does it return a number? I'm using V14.0 on Windows. $\endgroup$
    – houzw
    Commented Aug 6 at 18:12
  • $\begingroup$ I'm using V14.1 on a Mac. I'm not sure why they would change to approximate methods from exact ones. Also, the difference from 0 seems rather large. If it's a small machine-precision rounding error, it means the coordinates were on the order of 10^9 or 10^10. It's curious. -- Note the explicit question is, "How can I create a scene where such conclusion can appear?" (I suppose the OP wants this to help them in trying...to prove the result.) $\endgroup$
    – Michael E2
    Commented Aug 6 at 18:20
2
$\begingroup$ 
G = RandomInstance[
   GeometricScene[{a, b, c, d, e, f}, {d == Midpoint[{a, b}], 
     e == Midpoint[{b, c}], f == Midpoint[{c, a}], 
     Triangle[{a, b, c}], Line[{a, e}], Line[{b, f}], Line[{c, d}]}]];

Not entirely satisfactorily but using the points in G:

Chop@((d - c) + (f - b) + (e - a) /. G["Points"] ) == {0, 0}

True

Improve this answer
$\endgroup$
2
  • $\begingroup$ Interesting that there are other ways of using this, I thought that we could only use this by combining GeometricScene and FindGeometricConjectures. Is there a way to make FindGeometricConjectures yield this conclusion or at least something equivalent to it? $\endgroup$
    – Red Banana
    Commented Aug 14, 2023 at 21:06
  • $\begingroup$ Perhaps there is, but I don't know how to use vectors with a GeometricScene. $\endgroup$
    – Syed
    Commented Aug 15, 2023 at 1:14

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Not the answer you're looking for? Browse other questions tagged or ask your own question.