Es besorgt mich wirklich, wie viele Mathematiker mir diese Woche gesagt haben: "Wenn es in Lean kompiliert, wissen wir, dass es wahr ist." Lean ist großartig, aber das ist gefährlich unwahr. Hier sind 50 Möglichkeiten, 1 == 0 in Lean zu beweisen. Die kompilieren. Je nachdem, welche Version Sie verwenden. (Link in den Kommentaren)