Thanks for posting these conversations here, in case people come into this chat room trying to find a way to search for formulas, it can be helpful to them obviously. To me it is also a great incentive to keep working on it.

BTW. Today, I also find a conversation (from Terence Tao) that spurs me to keep improving approach0. Here is the screenshot: imgur.com/a/Cvtt4TS