Category Archives: undergrad maths

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

Mathematics in type theory.

An explanation of how to set up mathematics using universes, types, and terms Continue reading

Posted in Learning Lean, Type theory, undergrad maths | Tagged , , , | 24 Comments

The complex number game

The complex number game, and the Xena Project’s first steps into Twitch and Discord. Continue reading

Posted in General, Learning Lean, undergrad maths | Tagged , | 4 Comments

Xena Project Thursday meetings start with talk tomorrow 21st May

The Complex Number Game — proving basic stuff about the complexes in Lean Continue reading

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

Summer projects 2020

Undergraduate mathematician? Not much to do in July and August? Come and work with me! Continue reading

Posted in Imperial, Learning Lean, Uncategorized, undergrad maths | Tagged , | 2 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

Where is the fashionable mathematics?

A challenge to the users of all the computer proof systems to do some modern mathematics. Continue reading

Posted in Algebraic Geometry, General, Learning Lean, undergrad maths | Tagged | 18 Comments

My algebraic geometry course

The union of two affine algebraic sets is an affine algebraic set. Continue reading

Posted in Algebraic Geometry, Imperial, Learning Lean, M4P33, undergrad maths | Tagged , , | 3 Comments