What software do you use to accurately draw geometry diagrams?
[Math] Software for drawing geometry diagrams
big-listgeometrymath-software
Related Solutions
This is just a special case of automated theorem proving. A nice thing is some geometry problem can indeed be solved by an algorithm.
There are theories show such system can be realized algorithmically. I don't know if anyone have really wrote the program to do it. JGEX seems to do that.
A mechanical geometry proof technique was popularized in China by Jingzhong Zhang. He first introduced it as a way for machines to solve geometric problems relating the proportions between areas, lengths or angles. Then some Olympiad people I know start using it to bash that kind of problem. I don't know what the name is in English, but a literal translation of the method is "point removal method". Although it's not exactly same as what you are talking about, because "input a geometry problem" requires you to provide the construction of the problem from a straight edge and a compass, which is almost like "manually converting to equations".
the basic idea:
Construct the original problem by compass and straightedge, make a list of every constructed point ordered by the order of construction, let it be L. Record which points are used in the construction of every point.(Only the points used to construct point P are used in the substitution steps 3 and 4)
Translate the theorem into a equivalent form. Usually a/b = 1, where a and b are functions of length and area of certain segments or triangles. Let's call this equation E.
Let P be the last point of L. For every P appears in E, substitute it with another relation using other points from L(P itself is also allowed), usually if we are proving about lengths, we might use area. A list of possible operations are required for this step. It can branches off as a proof tree when the program decide to use different substitutions.
Do another substitution that eliminates the point P. For example, if in the step before, we substitute length to area, then we want to find something involve the length.
Do 3 to 4 over and over until we have 1=1
An example:
Angle bisector theorem
Given: $AD$ is the angle bisector of $\angle BAC$ of triangle $\triangle ABC$. Let $XYZ$ be the area of triangle $\triangle XYZ$, and $XY$ be the length of segment $XY$.
Prove: $\frac{AB}{AC} = \frac{BD}{DC}$
Proof:
First construct $ABC$. Then construct $AD$. The points in the list $L$ are $A,B,C,D$.
The equivalent equation to the theorem is $\frac{AB}{AC} \frac{DC}{BD} = 1$
$\frac{AB}{AC} \frac{DC}{BD} = \frac{AB}{AC} \frac{ACD}{ABD}$ (substitute length with area)
$=\frac{AB}{AC} \frac{\frac{1}{2} AC\cdot AD \sin \angle CAD}{\frac{1}{2} AB\cdot AD \sin \angle BAD}$, this step successfully remove point $D$ by cancellation.
$=\frac{AB}{AC} \frac{AC}{AB} =1$
This is only a non-formal explanation of how such automated system would work. I think the following book from Zhang will tell you more about it: Machine proofs in geometry: automated production of readable proofs for geometry theorems. I did not read the book, but the description of it seems like what you are seeking. A few paper by Zhang and his colleague can be found in the JGEX's website. The JGEX documentation on it's automated theorem prover is also a great resource.
GeoGebra 5.0 (with 3D) has been released:
Best Answer
For geometry I've always used Geogebra, and I think it's pretty good.