On generating "free" information

Stream: Lean Together 2021

[Jacques Carette]

I figured I should also dispell something that might be misunderstood from our approach: we do not claim that our way of doing things is the way of doing it.

The most important point is: there is a huge amount of redundancy in math libraries. And computers are really very very good at dealing with redundancy. And there is some existing meta-mathematics, and some to-be-done meta-mathematics, that can tell us that this redundancy is not an illusion but really is structural. So it should be leveraged.

Thus we should be actively working towards making sure that humans don't have to do work that is automatable. And find ways to augment our meta-mathematics to really use that structure to its fullest.

If someone decided that the way we're doing things is all wrong, and provided a better, more elegant way to do things, as long as they cite us :smile: , I would consider that a total win!

It is however very important to differentiate between information obtainable for free, and information that is true but requires a trivial but non-uniform proof. For example, that preservation of unit in a group is not needed in the definition of homomorphism, because it is derivable. One should not expect a uniform mechanism to deal with that, as that is not 'free'.