Tag Archives: Jeremy Avigad
Lean Together 2020
Thoughts on the talks at FoMM/Lean Together 2020 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