On Mar 6, 2014, at 11:06 PM, Joe Niederberger <firstname.lastname@example.org> wrote:
> Univalent Foundations is a new area of research which aims to help to reconnect these streams with a particular focus on the development of > software for building rigorously verified constructive proofs and models using abstract mathematical concepts. > This is of course a very long term project and we can not see today how its end points will look like. I will concentrate instead its recent history, current stage and some of the short term future plans.?
This is interesting. I also came across a notion awhile back, that I found very interesting, but haven?t seen it again since. Essentially, it had to do with taking a mathematical theorem, re-representing it in a discrete program, proving the program, and thus proving the theorem. I don?t have any more detail.