Tag Archives: Isabelle-HOL

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 , , , , , | 2 Comments

Rigorous mathematics

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

Posted in rigour, Uncategorized | Tagged , , , , , , , , , , , , , , , , , , , , | 13 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 , , , , , , , , , , , , , , , , | 7 Comments