News for hackers. Stuff that matters.

A comment on OpenAI Codex. Parent comment

Re:OpenAI Codex by hakuseki on Tuesday August 10, 2021 @07:56PM (#28136305)
What about GPT-f? It's a language model that proved theorems in the metamath formal system.
[ Parent | on HN ]
Re:OpenAI Codex by 6gvONxR4sf7o on Tuesday August 10, 2021 @08:16PM (#28136444)
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.
[ Parent | on HN ]