alt Hacker NewsIt's completely different things. Math itself is abstraction. Lean is formalized abstraction that don't let you write "it is immediately obvious that"
Replies
markburns • today at 8:37 AM
Knowing very little about lean but speculating here: is lean something that could output a few natural language expressions at key points so that you can still have “it should be clear that” for the natural language reader but have it undeniably proven.
Ie entrust the more tedious aspects but be able to follow along and still have references to check if you are curious about thoroughness.
Almost like a tap with a latex renderer at various insertion points?
Lean tactics can handle obvious things automatically, for some value of "obvious".