Intro: Vadim

Stream: new members

[Vadim Fomin]

Hi everyone,
My name is Vadim. By profession, I do NLP, which is to say I teach neural networks to work with texts.
I recently got interested in the topic of proof-assistants. I think this community is very inspiring, because it makes new infrastructure for creating and storing knowledge.
I have a little project that I'd like to develop on top of Lean. Can anyone point me to how to talk to Lean in Python? (Like a nice wrapper, or starting a server and talking via API, or something).
Additionally, would anyone be interested in doing a little coding with me? (Skill context: I'm not super deep into Lean, although I did pass the Natural Numbers Game)

[Patrick Massot]

You should probably have a look at what happens in the https://leanprover.zulipchat.com/#narrow/stream/219941-Machine-Learning-for-Theorem-Proving stream