| ▲ | Reubend 8 hours ago |
| It's great that important discoveries like this can now routinely be accompanies by formalized proofs. The fact that it's being released alongside a Lean proof from Day 1, rather than the Lean proof being released months or years later, is super helpful for verifying that it's correct. |
|
| ▲ | imbusy111 8 hours ago | parent [-] |
| I feel sorry for whoever has to read and understand the solution. It looks like the typical convoluted unreadable mess I see the models generate for software. It might be technically correct, but gaining insight from it is just intellectual hell. |
| |
| ▲ | nradov 7 hours ago | parent | next [-] | | There's an opportunity to build a Lean "optimizer" which automatically simplifies existing proofs. | | |
| ▲ | stabbles 7 hours ago | parent [-] | | Yeah, code golfing for lean would be amazing, especially if they can make the proof to Fourier's Last Theorem fit in the margin. Extra credits if it is proven that the proof cannot be reduced any further. |
| |
| ▲ | rfgplk 8 hours ago | parent | prev [-] | | Skill issue. Also lean is meant to be executed, not read. | | |
| ▲ | professoretc 6 hours ago | parent | next [-] | | A proof is not like a program. The goal of a program is to "do the thing", thus you can make the argument that it doesn't matter what the code looks like as long as its works right. But the goal of a proof isn't to "do the thing" (where "the thing" is just to print Yes or No), it's to communicate. An unintelligible proof is really just a first draft. | | | |
| ▲ | oinoom 6 hours ago | parent | prev | next [-] | | its important to read it anyway because there have been and will continue to be errors in the construction of the proof software itself. which leads ai and humans alike to prove things that arent true | |
| ▲ | arodev 7 hours ago | parent | prev [-] | | i think they're talking about the writeup |
|
|
