3 ms·

lean compiles or it doesnt

• whattheheckheck 4mo ago
  You can also pass pytest with assert 1 = 1...
  • 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 ago
      Are 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.