Lean aims to bring two worlds together
"By relieving the brain of all unnecessary work, a good notation sets it free to concentrate on more advanced problems, and in effect increases the mental power of the race." – A. N. Whitehead
Lean has an efficient bytecode interpreter
Building an equality predicate for each new type is very tedious.
We implemented a tactic in Lean (< 100 lines) that creates these instances automatically.
Resolution prover (Gabriel Ebner)
[g : comm_group A], suppose we want to apply the theorem
right_commto the following term as a rewriting rule.
[s : comm_semigroup A]?
?a * ?bwith
x * y