[kimjune01]

lean compiles or it doesnt

[whattheheckheck]

You can also pass pytest with assert 1 = 1...

[pfdietz]

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.