# Tag Archives: lean

## Half a year of the Liquid Tensor Experiment: Amazing developments

[This is a guest post by Peter Scholze.] Exactly half a year ago I wrote the Liquid Tensor Experiment blog post, challenging the formalization of a difficult foundational theorem from my Analytic Geometry lecture notes on joint work with Dustin … Continue reading

## Mathematics in type theory.

An explanation of how to set up mathematics using universes, types, and terms 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 does not (yet) have real manifolds.

Lean does not yet have real manifolds, but there has been recent progress. Continue reading

Posted in General, Imperial, undergrad maths
Tagged Agda, Bochner Integral, Coq, HOL-Light, Idris, Isabelle-HOL, Jeremy Avigad, Johan Commelin, lean, manifold, Mizar, Patrick Massot, Perfectoid Spaces, Sebastien Gouezel, theorem provers, UniMath, Zhouhang Zhou
7 Comments