Tag Archives: Coq
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
Posted in General Tagged Arend, Coq, Isabelle-HOL, lean, Mizar, UniMath 2 Comments
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