I feel increasingly anxious reading this. Machine research shouldn’t be merged into mainline of human knowledge.

When you can formalize it in Lean or some such, why would this be? I can understand the desire to separate out other forms of research from the human corpus. But theoretical math that is decidable/provable, I’m not sure I see the risks.

Why?

Knowledge is knowledge, as long as it can be proven true.