If this is legit, this is huge. Finding geometric proofs means proving things, and proving propositions is what an intelligence does. In my opinion, this is the closest we have gotten so far to AGI. Really excited to see what the future holds.
This is not a pure LLM. Search algorithms are obviously incredibly powerful at solving search problems. The LLM contribution is an "intuitive" way to optimize the search.
> When producing full natural-language proofs on IMO-AG-30, however, GPT-4 has a success rate of 0% ...
Have you tried the same questions with ChatGPT 4? It is a transformational change (no pun intended) over the earlier releases, and over all open-source models.
Just today, I needed to interpret some awkwardly-timestamped log data. I asked it a few questions along the lines of "What time it was 10,000 seconds before xx:yy:zz?" It didn't give me the answer, but it wrote and executed a Python program that did.
> When producing full natural-language proofs on IMO-AG-30, however, GPT-4 has a success rate of 0% ...
News flash: either AI gains the ability to postulate theorems, generate proofs, and validate them, or mathematics is as dead as Latin. Humans have reached their limit.