Tag Archives: london school of geometry and number theory

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