Category Archives: undergrad maths

The trace of an endomorphism (without picking a basis)

Did you pick a basis when doing a linear algebra question about finite-dimensional vector spaces? Did you need to? Depends on what you mean. Continue reading

Posted in computability, undergrad maths | Tagged , | 16 Comments

Induction on equality

In type theory, equality has a definition, and basic facts about it such as symmetry and transitivity can be proved from more fundamental principles. Continue reading

Posted in M1F, M40001, Type theory, undergrad maths | Tagged , | 8 Comments

Formalising Mathematics : workshop 7 — quotients

Is a quotient a set of equivalence classes? I think it’s something a bit more general than that. Continue reading

Posted in formalising mathematics course, M1F, undergrad maths | Tagged , | 7 Comments

Formalising Mathematics : workshop 5 — filters

What is a filter on a set? I am kind of getting the hang of it now. Continue reading

Posted in formalising mathematics course, Imperial, undergrad maths | Tagged , | 5 Comments

Formalising Mathematics : workshop 4 — topology

OK, an overview of this week: we’re doing topology. I was going to introduce filters but I decided to put them off for one more week, so this week it’s topology the way it is traditionally taught in mathematics departments. … Continue reading

Posted in formalising mathematics course, Learning Lean, tactics, undergrad maths | Leave a comment

Formalising mathematics : workshop 3 — sequences and limits

This week we’re going to do limits of sequences, of the kind you see in a 1st year analysis course. These are great fun to do in Lean. Because of Rob Lewis’ linarith tactic (which does the “and now this … Continue reading

Posted in formalising mathematics course, M1P1, undergrad maths | 1 Comment

Formalising mathematics : Workshop 2 — groups and subgroups

This is some notes on the second workshop in my Formalising Mathematics course, running as part of the EPSRC TCC. The Lean github repo is here. Groups and subgroups I start with an apology — there was far too much … Continue reading

Posted in formalising mathematics course, undergrad maths | Leave a comment

The end of the summer.

It’s the end of the summer now, so it must finally be time to talk about the summer projects, and the things which happened since then. Continue reading

Posted in Imperial, Learning Lean, M40001, undergrad maths | Tagged | Leave a comment

Thoughts on the Pythagorean theorem

Pythagoras’ theorem says that a square is equal to two squares. What does equality mean here? Continue reading

Posted in General, Olympiad stuff, Type theory, undergrad maths | Tagged , , | 8 Comments

Division by zero in type theory: a FAQ

How can a theorem prover use the convention that 1/0=0 and still be consistent? Continue reading

Posted in Learning Lean, M1F, M40001, Type theory, undergrad maths | Tagged , | 12 Comments