elikoga

Stream: new members

[Eli Kogan-Wang]

I had the joy to listen to the Weierstraß Lecture about analytic geometry by Peter Scholze and I was very pleasantly surprised to hear about Lean being used to formalize a theorem used, since I played around with Coq when I was still in school and am still interested in Type-Theoretic Proof assistants

Lean seems like a much better documented community/software than coq

I'd love to contribute somewhere in the future

[Kevin Buzzard]

Hi! It's perhaps better documented for mathematicians; I think there is plenty of Coq documentation which is more computer-science focussed. One of the things we're trying to do here is to have a maths library which is capable of understanding at least at lot of the statements of the theorems of modern mathematics, and for this to work it's important that mathematicians can get on board!