# 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