GPT-3 codex for maths?

Stream: general

[Mario Carneiro]

There's a whole stream dedicated to this topic: #Machine Learning for Theorem Proving

[Jason Rute]

I don’t know enough about Codex yet, but you may be interested in Lean gpt-f which itself is a collaboration with Stan Polu at Open-AI. Stan and Jesse Han and others are working on a number of projects applying AI to theorem proving. Here are some resources on Lean gpt-f.

• steam: #lean-gptf
• paper: https://arxiv.org/abs/2102.06203
• repo: https://github.com/jesse-michael-han/lean-gptf
• short talk: https://iclr.cc/virtual/2021/workshop/2124#collapse-sl-3634
• long talk: https://m.youtube.com/watch?v=EXpmbAfBNnw