Comment by auggierose

Quite flawed, but inspired. This stuff popping up is interesting. I guess it is due to Lean reaching people that would not be aware of formal reasoning on a computer before.