Hacker News Reader

What about GPT-f? It's a language model that proved theorems in the metamath formal system.

I'd definitely say it understands those theorems with respect to the metamath formal system then. The next question is what it understands the proofs with respect to.

Reply on news.ycombinator.com