Category Archives: Learning Lean

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

No errors.

Does your Lean file contain errors? Try and cut down. Continue reading

Posted in Learning Lean, Technical assistance, Uncategorized | Tagged , , , | Leave a comment

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 | 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 , , | 3 Comments

Prove a theorem. Write a function.

New maths PhD students Lambert A’Campo and Ashvni Narayanan have proved that a normed real vector space with compact unit ball is finite-dimensional in Lean! [update added a few days later: ROFL Sébastien Gouëzel on the Lean chat complained that … Continue reading

Advertisement

Posted in General, Imperial, Learning Lean | Tagged , , , , , , , , | 6 Comments

The natural number game — an update

I just pushed an update to the natural number game. I’m rather pleased with how this has all worked out. I started off thinking it was kind of a game, but the explanations turned out so wordy and now I … Continue reading

Posted in Learning Lean, M40001, undergrad maths | Tagged , | 22 Comments

Chalkdust, and the natural number game!

Ever wanted to prove x+y=y+x but couldn’t be bothered to download and install a computer theorem prover? Well now you can! Continue reading

Posted in Learning Lean, undergrad maths | Tagged , , , | 13 Comments

The inverse of a bijection.

Constructing the inverse of a bijection in Lean can be tricky for beginners. Continue reading

Posted in Learning Lean, M1F | Tagged , | 9 Comments

Equality part 2: syntactic equality

Syntactic equality is yet another kind of equality. I am beginning to learn why it matters. Continue reading

Posted in Learning Lean, tactics | Tagged , | Leave a comment

Equality part 1: definitional equality.

I keep meaning to write something about equality in Lean, and on the tube home today I just managed to understand it a little bit better, so perhaps now is the time (although I won’t get to today’s revelation until … Continue reading

Posted in Learning Lean | Tagged , | 2 Comments