Hacker News new | past | comments | ask | show | jobs | submit
evenhash | on: An OpenAI model has disproved a central conjecture in discrete geometry
The proof is not written in Lean, though. It’s written in English and requires validation by human experts to confirm that it’s not gibberish.
vatsachak | parent
Yeah, but I wouldn't be surprised if they train the model on verification assisted by Lean