# Tag Archives: lean

## The Future of Interactive Theorem Proving?

This is a guest post, written by Zhangir Azerbayev. Zhangir is an undergraduate at Yale, majoring in computer science and mathematics. He completed this work while visiting Carnegie Mellon’s Hoskinson Center for Formal Mathematics. Introduction The history of interactive theorem … Continue reading

## 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