Tag Archives: Tim Gowers

Two types of universe for two types of mathematician

Thank you Johan for pointing out to me that the mathlib stats page had got really good! But one thing that made me laugh is that somehow on their stats for commits I see I have done just enough to … Continue reading

Posted in Uncategorized | Tagged , , | 9 Comments

The invisible map

Is a subgroup of a group a group? Is 3 a topology on 2? Is a natural number a real number? Decisions like this have consequences. Continue reading

Posted in Type theory, undergrad maths | Tagged , , , | 7 Comments