New result: GPT for formal theorem proving. We produced shorter proofs of existing theorems (github.com/metamath/set.mm/p…), and proofs of assertions people hadn't yet written formal proofs for (github.com/metamath/set.mm/p…), which have been merged into the Metamath proof database.

Shortening of various proofs based on OpenAI's provers by spolu · Pull Request #1547 · metamath/s...

This PR proposes various shorter versions of proofs discovered by automated reasoning models developed at OpenAI. We focused on proofs that were substantially shortened and not marked as discourage...

github.com
Stanislas Polu
 @spolu
9 Sep 2020
Posted my first paper on arXiv💥🙌 GPT-f is a Transformer-based automated theorem prover. We show that Transformer + Search is suitable to formal reasoning and continuous self-improvement 🦾 arxiv.org/abs/2009.03393

Sep 9, 2020 · 7:08 PM UTC

4
73
11
299
Replying to @gdb
That's superexciting!
Replying to @gdb
Cool, harbinger of new knowledge including in applied math.
Replying to @gdb
Damn. Is there anything big enough transformer cannot do? Great work.
3
Replying to @gdb @walterdebrouwer
That would mean that Hilbert and Ackerman’s challenge is met. Revolutionary moment or only self-delusional. Allow me to take time to evaluate the claim and the proof in detail.
1