3 ms·
There are also ways to cheat like that in Lean, but they are all easily identifiable. So when people talk about formalization, they mean formalization without
by pfdietz 4mo ago
There are also ways to cheat like that in Lean, but they are all easily identifiable. So when people talk about formalization, they mean formalization without such cheats.
- tripzilch 4mo agoAre you sure? If an AI would generate a huge Lean proof/program, wouldn't there be a way to hide such cheats in it? Like as in the underhanded C contest? Because if you give an AI a goal, and cheating at Lean would satisfy that goal, the AI will do it if it can figure it out.
- pfdietz 4mo ago> wouldn't there be a way to hide such cheats in it? No.