Tag Archives: Peter Scholze

Liquid tensor experiment

Peter Scholze suggests a mathematical formalization challenge. Continue reading

Posted in number theory | Tagged , | 11 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 , , , , , , , , , , , , , , , , , , , , | 10 Comments

Prove a theorem. Write a function.

New maths PhD students Lambert A’Campo and Ashvni Narayanan have proved that a normed real vector space with compact unit ball is finite-dimensional in Lean! [update added a few days later: ROFL Sébastien Gouëzel on the Lean chat complained that … Continue reading

Posted in General, Imperial, Learning Lean | Tagged , , , , , , , , | 6 Comments