Tag Archives: Ashvni Narayanan

Prove a theorem. Write a function.

Posted on December 7, 2019 by xenaproject

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 Ashvni Narayanan, canonical, collection, compact unit ball, etale cohomology, Grothendieck topology, london school of geometry and number theory, LSGNT, Peter Scholze | 6 Comments

Tag Archives: Ashvni Narayanan

Prove a theorem. Write a function.

Categories

Recent Posts