# Posts in the category Formalization

### The dawn of formalized mathematics

- 24 June 2021
- Talks, Formalization

Here are the slides of my talk "The dawn of formalized mathematics" from the 8th European Congress of Mathematics, which is taking place online and in Protorož, Slovenia, from June 20 to 26, 2021:

**Keynote presentation**, viewable online in your browser. Turn on the speaker notes by clicking on the rectangular icon in the top-left corner.**Slides with speaker notes**(PDF). Unfortunately, Keynote does not make the hyperlinks active when exporting PDF.**Video recording**of the talk.

### 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