Tag Archives: Peter Scholze

Lean 2022 round-up

A brief survey post containing some of the things which happened in the Lean community in 2022. The Liquid Tensor Experiment In December 2020, Fields Medallist Peter Scholze challenged the formal computer proof community to verify one of his theorems … Continue reading

Advertisement

Posted in Uncategorized | Tagged , , , , | 2 Comments

Beyond the Liquid Tensor Experiment

The liquid tensor experiment is now fully completed. Continue reading

Posted in Algebraic Geometry, liquid tensor experiment | Tagged , | 4 Comments

Half a year of the Liquid Tensor Experiment: Amazing developments

[This is a guest post by Peter Scholze.] Exactly half a year ago I wrote the Liquid Tensor Experiment blog post, challenging the formalization of a difficult foundational theorem from my Analytic Geometry lecture notes on joint work with Dustin … Continue reading

Posted in Uncategorized | Tagged , , | 22 Comments

Liquid tensor experiment

Peter Scholze suggests a mathematical formalization challenge. Continue reading

Posted in number theory | Tagged , | 16 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

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