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

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.

• – Amzoti Dec 19 '13 at 3:22
• I'm more interested in diagram-generating software than software that generates the solutions to problems. – okarin Dec 19 '13 at 3:23
• See the second entry, but the first ones can solve problems and have very powerful tools for what you need too. – Amzoti Dec 19 '13 at 3:24
• I don't understand how a diagram can be used in a formal proof. Isn't a formal proof just a big long list of words in some formal language that follow certain rules? – dfeuer Dec 19 '13 at 4:10
• @user112825 Please check Amzoti's link. $\LaTeX$ can produce any diagram you want. You can guess how easy it is. PSTricks can produce excellent diagrams. Not easy either, but there is at least one excellent book on it, and probably tons of free online. Maple can produce good diagrams if you have the software and you are good at it. It is easy to find help with Maple. Maple is closer to being WYSIWYG than PSTricks. Photoshop is nice because it is WYSIWYG but I think it is expensive, and probably not worth obtaining for math diagram purposes if you don't already have it. – Stefan Smith Dec 19 '13 at 5:20

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}

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. :)  