Category Archives: General
Thoughts on the Pythagorean theorem
Pythagoras’ theorem says that a square is equal to two squares. What does equality mean here? Continue reading
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
The complex number game
The complex number game, and the Xena Project’s first steps into Twitch and Discord. Continue reading
Where is the fashionable mathematics?
A challenge to the users of all the computer proof systems to do some modern mathematics. Continue reading
Lean is better for proper maths than all the other theorem provers
How well can modern computer proof verification systems handle the statements of modern mathematics? We don’t know. Let’s find out. Continue reading
Lean Together 2020
Thoughts on the talks at FoMM/Lean Together 2020 Continue reading
Lean has real manifolds!
Lean has real manifolds — and tangent bundles too! Continue reading
My visit to Microsoft Research
A brief account of my visit to Microsoft Research Continue reading
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
IMO 2019 Q1
Thoughts on doing an IMO problem in Lean Continue reading
Xena 