Automated generation of illustrated proofs in geometry and beyond

Abstract

Illustrations are only rarely formal components of mathematical proofs, however they are often very important for understanding proofs. Illustrations are almost unavoidable in geometry, and in many other fields illustrations are helpful for carrying ideas in a more suitable way than via words or formulas. The question is: if we want to automate theorem proving, can we automate creation of corresponding illustrations too? We report on a new, generic, simple, and flexible approach for automated generation of illustrated proofs. The proofs are generated using Larus, an automated prover for coherent logic, and corresponding illustrations are generated in the GCLC language. Animated illustrations are also supported.