Posts in the category Formalization
- 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