MathWiki conference III

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.


Tags: ,

Leave a Reply

Fill in your details below or click an icon to log in: Logo

You are commenting using your account. Log Out /  Change )

Twitter picture

You are commenting using your Twitter account. Log Out /  Change )

Facebook photo

You are commenting using your Facebook account. Log Out /  Change )

Connecting to %s

This site uses Akismet to reduce spam. Learn how your comment data is processed.

%d bloggers like this: