Aarne Ranta on Formal Mathematics in Informal Language
This talk considers generating readable prezentations of formalized mathematics as a special case of parsing and generating natural language statements. It looks like the idea is to translate at least formal definitions and statements, and perhaps also proofs, into the GF language, then generate natural language(s) reprezentation from that.
The talk is more about computer-supported linguistics than mathematics so I don’t want to pretend I understand what is on the slides. Some interesting comments from the author can be found on his blog.
Cezary Kaliszyk on teaching logic using web interface for COQ
The slides are actually about a bit more than the title says. Cezary’s web interface to provers is the closest thing to the formalized math wiki that exists. It is quite generic and besides COQ it supports (at least) Isabelle back end. It even supports Isabelle/ZF so it already can be used for learning the prover without having to install it. I was not able to verify IsarMathLib theories though as the interface seems to have problems with mixing formal text, informal text and comments.