Category Archives: Algebraic Geometry

Equality, specifications, and implementations

There are lots of kinds of equalities in Lean. Here’s some basic things that a mathematician needs to know to understand what’s going on Continue reading

Posted in Algebraic Geometry, General, Type theory | Tagged , , | 6 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