We study formal proofs conceived to be checked automatically. These proofs are rarely used. We think that it is partly due to the fact that it is very difficult for a human to understand the connection between what he considers a mathematical proof and its formal representation. We are interested in automatically producing text explaining these formal representations. We have chosen to produce text in natural language using the traditional vocabulary of mathematics.
展开▼
