What software is useful for generating diagrams to use in formal proofs?

Question

What software is useful for generating diagrams to use in formal proofs? I am interested in software for geometry diagrams, graphs, plots, and any other useful kinds of diagrams.

Answer 1

Try downloading Geogebra. You can make nice diagrams in there. Also, if you are using LaTeX to type your solutions, you can export the Tikz code from Geogebra by File >> Export >> Graphics View as PGF/Tikz.

An example of something I created in Geogebra recently is

When exporting the code from Geogebra, I get what is below. It would be a HUGE pain to generate this by hang, but Geogebra does it all for you.

\begin{tikzpicture}[line cap=round,line join=round,>=triangle 45,x=1.0cm,y=1.0cm] \clip(-4.3,-2.8) rectangle (12.1,3); \draw(0,0) circle (2cm); \draw [shift={(0.23,1.18)}] plot[domain=3.07:5.73,variable=\t]({1*0.57*cos(\t r)+0*0.57*sin(\t r)},{0*0.57*cos(\t r)+1*0.57*sin(\t r)}); \draw [shift={(0.12,0.72)}] plot[domain=-0.2:2.85,variable=\t]({1*0.35*cos(\t r)+0*0.35*sin(\t r)},{0*0.35*cos(\t r)+1*0.35*sin(\t r)}); \draw [shift={(-3.85,-0.05)}] plot[domain=-1.03:1.13,variable=\t]({1*1.85*cos(\t r)+0*1.85*sin(\t r)},{0*1.85*cos(\t r)+1*1.85*sin(\t r)}); \draw [shift={(-4.34,-0.93)}] plot[domain=-0.77:0.91,variable=\t]({1*2.09*cos(\t r)+0*2.09*sin(\t r)},{0*2.09*cos(\t r)+1*2.09*sin(\t r)}); \draw (-3.06,0.72)-- (-3.06,1.62); \draw (-2.9,-1.64)-- (-2.84,-2.38); \draw (-0.16,2.94) node[anchor=north west] {$$A$$}; \draw(5,0) circle (2cm); \draw [shift={(9.02,-0.4)}] plot[domain=1.88:4.31,variable=\t]({1*2.06*cos(\t r)+0*2.06*sin(\t r)},{0*2.06*cos(\t r)+1*2.06*sin(\t r)}); \draw [shift={(9.3,-1.06)}] plot[domain=2.03:4.15,variable=\t]({1*2.08*cos(\t r)+0*2.08*sin(\t r)},{0*2.08*cos(\t r)+1*2.08*sin(\t r)}); \draw (8.4,1.56)-- (8.38,0.8); \draw [shift={(5.11,1.14)}] plot[domain=3.07:5.73,variable=\t]({1*0.57*cos(\t r)+0*0.57*sin(\t r)},{0*0.57*cos(\t r)+1*0.57*sin(\t r)}); \draw [shift={(5,0.68)}] plot[domain=-0.2:2.85,variable=\t]({1*0.35*cos(\t r)+0*0.35*sin(\t r)},{0*0.35*cos(\t r)+1*0.35*sin(\t r)}); \draw (5,2.78) node[anchor=north west] {$$B$$}; \draw (8.22,-2.3)-- (8.2,-2.82); \begin{scriptsize} \fill [color=uuuuuu] (-2,0) circle (2.5pt); \fill [color=black] (7,0) circle (2.5pt); \end{scriptsize} \end{tikzpicture}

Answer 2

I suggest you using the Interactive Geometry Software Cinderella . It helped me a lot when I was working on a problem given to me by a student 2 years ago. It, not only, can do the geometric plots in Euclidean Geometry but also in Hyperbolic platforms as well. Since, it's removed from my machine so I could post you some of its platform from Google. Try it. :)