Category Archives: General

General topics concerning constructive and computable mathematics.

How to review formalized mathematics

Recently I reviewed a paper in which most proofs were done in a proof assistant. Yes, the machine guaranteed that the proofs were correct, but I still had to make sure that the authors correctly formulated their definitions and theorems, that the code did not contain hidden assumptions, that there were no unfinished proofs, and so on.

In a typical situation an author submits a paper accompanied with some source code which contains the formalized parts of the work. Sometimes the code is enclosed with the paper, and sometimes it is available for download somewhere. It is easy to ignore the code! The journal finds it difficult to archive the code, the editor naturally focuses on the paper itself, the reviewer trusts the authors and the proof assistant, and the authors are tempted not to mention dirty little secrets about their code. If the proponents of formalized mathematics want to avert a disaster that could destroy their efforts in a single blow, they must adopt a set of rules that will ensure high standards. There is much more to trusting a piece of formalized mathematics than just running it through a proof checker.

Continue reading

The HoTT book

The HoTT book is finished!

Since spring, and even before that, I have participated in a great collaborative effort on writing a book on Homotopy Type Theory. It is finally finished and ready for public consumption. You can get the book freely at http://homotopytypetheory.org/book/. Mike Shulman has written about the contents of the book, so I am not going to repeat that here. Instead, I would like to comment on the socio-technological aspects of making the book, and in particular about what we learned from open-source community about collaborative research.

Continue reading

4WFTop and HDACT

This is an advertisement for two great meetings we are organizing in Ljubljana from June 15 to June 20, 2012:

There are many reasons why you should come: Ljubljana is lovely in June, with many cafes and restaurants on the Ljubljanica river bank, we have a very interesting programme, and when will you next be able to attend a meeting in which the keynote speakers are Per Martin-Löf, Ieke Moerdijk and Vladimir Voevodsky? Not to mention that the schedule is fairly light, everything is within walking distance, and we are organizing dinners at some excellent restaurants.

If you decide to come, make sure to book a hotel early and register today!