# 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