Mathematics and Computation

A blog about mathematics for computers

Postsby categoryby yearall

Posts in the category Formalization

A while ago, my former student Chuangjie Xu and I computed an integer using a sheaf topos. For that purpose,

  1. we developed our mathematics constructively,
  2. we formalized our mathematics in Martin-Löf type theory, in Agda notation,
  3. we pressed a button, and
  4. after a few seconds we saw the integer we expected in front of us.

Well, it was a few seconds for the computer in steps (3)-(4), but three years for us in steps (1)-(2).

continue reading
Postsby categoryby yearall