![](data:image/svg+xml,<svg xmlns="http://www.w3.org/2000/svg" width="73" height="73"><rect fill-opacity="0"/></svg>)
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
How far do you think we are from solving IMO problems? imo-grand-challenge.github.i… When I look at the theorems, like (n+1)/2 \in N => n = 2m+1, it seems like we are a very long way away. But this may be just the simple examples you've chosen to exhibit?
The examples are indeed extremely simple on purpose (otherwise it's hard to communicate efficiently what's happening to non Metamath experts).
That being said, we're still pretty far away from IMOs; but this is definitely a goal for us, and one we're actively working towards!
Sep 9, 2020 · 1:55 PM UTC