Category Archives: Algebraic Geometry
Beyond the Liquid Tensor Experiment
The liquid tensor experiment is now fully completed. Continue reading
Posted in Algebraic Geometry, liquid tensor experiment
Tagged liquid tensor experiment, Peter Scholze
4 Comments
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 equality, localisation, real numbers
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 fashionable mathematics
21 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 affine algebraic set, Algebraic Geometry, M4P33
3 Comments