Zulip Chat Archive

Stream: new members

Topic: elikoga

Eli Kogan-Wang (Jun 27 2022 at 14:08):

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 (Jun 27 2022 at 14:10):

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!

Last updated: Dec 20 2023 at 11:08 UTC