Tag Archives: manifold
Lean has real manifolds!
Lean has real manifolds — and tangent bundles too! Continue reading
The natural number game — an update
I just pushed an update to the natural number game. I’m rather pleased with how this has all worked out. I started off thinking it was kind of a game, but the explanations turned out so wordy and now I … 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
Xena 