Introducing GPT-AF

Stream: general

[Jason Rute]

We are excited to announce GPT-AF, a big step forward in auto-formalization. From just the English statement

The natural functorially induced map from the set of isomorphisms between two $NF$-bridges (respectively, two $\Theta$-bridges, two $\Theta N F$-Hodge theaters) to the set of isomorphisms between the respective associated $\mathcal{D}$-$NF$ -bridges (respectively, associated $\mathcal{D}$-$\Theta$-bridges; associated $\mathcal{D}$-$\Theta N F$-Hodge theaters) is bijective.

GPT-AF is able to formalize that statement into Lean code, supply all the missing definitions ($\mathcal{D}$-$\Theta$-bridges, $\mathcal{D}$-$\Theta N F$-Hodge theaters, bijective), and fill in complete Lean proofs broken into useful lemmas. It was trained only on Lean source code and a large body of mathematical literature from the Internet, using a cycle consistent Transformer. We also demonstrate this on other cutting-edge mathematical subjects such as stochastic differential equations, perfectoid spaces, and Inter-universal Teichmüller theory. Find out more here.