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
Xena 