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

\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}