codex

Stream: Machine Learning for Theorem Proving

[Kim Morrison]

I have occasionally found ChatGPT's codex is able to write useful Lean code, although it is very high latency.

Here's my setup script for the environment (using my fork of Mathlib).

The work I was most impressed by is #28533, where it actually managed to make non-trivial modifications to existing metaprogramming code.