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

Posted in General, Olympiad stuff, Type theory, undergrad maths | Tagged , , | 8 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 , , | 6 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

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

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

Posted in General | Tagged , , , , , | 2 Comments

Lean Together 2020

Thoughts on the talks at FoMM/Lean Together 2020 Continue reading

Posted in General | Tagged , , , , | 1 Comment

Lean has real manifolds!

Lean has real manifolds — and tangent bundles too! Continue reading

Posted in General, undergrad maths | Tagged , , | 5 Comments

My visit to Microsoft Research

A brief account of my visit to Microsoft Research Continue reading

Posted in General | Tagged , , | 2 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

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

IMO 2019 Q1

Thoughts on doing an IMO problem in Lean Continue reading

Posted in General, number theory, Olympiad stuff | Tagged , , | 6 Comments