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.
replyI just want to state that having "lean proofs" that build does not mean the actual real theorems we care about hold. Ultimately a human has to verify the lean encoded theorem statements that the lean proofs are checked against. For non-trivial theorems such as these, this is an arduous and tricky task where even a little mistake could be fatal.
replyWhy?
replyBecause science is a branch of philosophy and machine existence brings plethora of unanswered questions.
replyImagine humankind meets another race, another race shares it's scientific knowledge and humans accept it without experiencing process of discovery. In that case do we really got this knowledge? If we follow machine discoveries like we follow problems in textbook then we acquire knowledge but we don't discover anything. We follow.
There whole lot of philosophical questions that aren't attacked now. Are complex systems sentient because consciousness is emerging behavior? Then should they have rights? Philosophy is part of humanities and science (is/used to be) part of philosophy. Should we accept non-human knowledge in science? Maybe it's altogether different thing from science, yet very similar.
Knowledge is knowledge, as long as it can be proven true.
replyproving false is also useful
reply