alt Hacker News>You can still read and understand an AI written proof.
No you can't lol, they're multi million lines of Lean, which is already an obscure language to understand. It's an assault on your senses.
>You can still read and understand an AI written proof.
No you can't lol, they're multi million lines of Lean, which is already an obscure language to understand. It's an assault on your senses.
It's not only Lean code, there are English writeups too. To my understanding the pipeline for these problems is 1) solve in english 2) formalize systematically to check. No one is tackling problems purely in Lean, to my understanding.
https://cdn.openai.com/pdf/32d9f210-8b73-45e0-91bc-82a30aef8...