# Posts in the category Formalization

### Computing an integer using a Grothendieck topos

- 18 May 2021
- Constructive mathematics, Type theory, Formalization

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

- we developed our mathematics constructively,
- we formalized our mathematics in Martin-Löf type theory, in Agda notation,
- we pressed a button, and
- 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