Tag Archives: Coq

Lean is better for proper maths than all the other theorem provers

Posted on February 9, 2020 by xenaproject

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

Rigorous mathematics

Posted on December 7, 2019 by xenaproject

What is rigorous mathematics? Jaffe and Quinn have some ideas, which I re-interpret a little. Continue reading →

Posted in rigour, Uncategorized | Tagged Bill Thurston, Brian Conrad, Coq, David Hansen, Dominic Verity, Dustin Clausen, Emily Riehl, Frank Calegari, George Boxer, Isabelle-HOL, Jaffe and Quinn, Johan de Jong, metamath, Mizar, Mochizuki, Peter Scholze, rigour, Toby Gee, UniMath, Vincent Pilloni, ZFC | 13 Comments

Lean does not (yet) have real manifolds.

Posted on July 17, 2019 by xenaproject

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

Tag Archives: Coq

Lean is better for proper maths than all the other theorem provers

Rigorous mathematics

Lean does not (yet) have real manifolds.

Categories

Recent Posts