Connecting informal and formal mathematics by H.J. Elbers